Verifying and Analyzing Adaptive Logic through UML State Models Export

@proceedings{citeulike:3814692, abstract = {It is becoming increasingly important to be able to adapt an application's behavior at run time in response to changing requirements and environmental conditions. Adaptive programs are typically difficult to specify, design, and verify. A variety of conditions may trigger an adaptation, each of which may involve different types of adaptation mechanisms. In many cases, adaptive systems are concurrent, thus further exacerbating the complexity. Furthermore, it is important that adaptations do not put the system into an inconsistent state during or after adaptation. This paper presents an iterative approach to modeling and analyzing UML behavioral design models of adaptive systems, where the UML state diagrams are automatically translated into Promela code for analysis with the Spin model checker. The adaptive models are analyzed for adherence to both system invariants and properties that should hold during adaptation. We demonstrate this approach on applications for the mobile computing domain where we verify the design models against formally-specified properties.}, author = {Ramirez, A. J. and Cheng, B. H. C.}, booktitle = {Software Testing, Verification, and Validation, 2008 1st International Conference on}, citeulike-article-id = {3814692}, citeulike-linkout-0 = {http://dx.doi.org/10.1109/ICST.2008.67}, citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4539586}, doi = {10.1109/ICST.2008.67}, journal = {Software Testing, Verification, and Validation, 2008 1st International Conference on}, keywords = {2008, adaptive\_logics, analysis, statecharts, uml, verification}, pages = {529--532}, posted-at = {2008-12-20 16:19:14}, priority = {2}, title = {Verifying and Analyzing Adaptive Logic through UML State Models}, url = {http://dx.doi.org/10.1109/ICST.2008.67}, year = {2008} }

TY - CONF ID - citeulike:3814692 L3 - citeulike-article-id:3814692 N2 - It is becoming increasingly important to be able to adapt an application's behavior at run time in response to changing requirements and environmental conditions. Adaptive programs are typically difficult to specify, design, and verify. A variety of conditions may trigger an adaptation, each of which may involve different types of adaptation mechanisms. In many cases, adaptive systems are concurrent, thus further exacerbating the complexity. Furthermore, it is important that adaptations do not put the system into an inconsistent state during or after adaptation. This paper presents an iterative approach to modeling and analyzing UML behavioral design models of adaptive systems, where the UML state diagrams are automatically translated into Promela code for analysis with the Spin model checker. The adaptive models are analyzed for adherence to both system invariants and properties that should hold during adaptation. We demonstrate this approach on applications for the mobile computing domain where we verify the design models against formally-specified properties. JF - Software Testing, Verification, and Validation, 2008 1st International Conference on EP - 532 TI - Verifying and Analyzing Adaptive Logic through UML State Models T2 - Software Testing, Verification, and Validation, 2008 1st International Conference on SP - 529 KW - 2008 KW - adaptive_logics KW - analysis KW - statecharts KW - uml KW - verification AU - Ramirez, AJ AU - Cheng, BHC PY - 2008/// UR - http://dx.doi.org/10.1109/ICST.2008.67 ER -