Chapter Four
Optimizing the Symbolic Execution of Evolving Rhapsody Statecharts
Amal Khalil; Juergen Dingel School of Computing, Queen's University, Kingston, ON, Canada
Abstract
Model-driven engineering (MDE) is an iterative and incremental software development process. Supporting the analysis and the verification of software systems developed following the MDE paradigm requires to adopt incrementality when carrying out these crucial tasks in a more optimized way.
Communicating state machines are one of the various formalisms used in MDE tools to model and describe the behavior of distributed, concurrent, and real-time reactive systems (e.g., automotive and avionics systems). Modeling the overall behavior of such systems is carried out ...
