Z. Dong, Yujian Fu (USA), Yue Fu (PRC), and X. He (USA)
Software Architecture, Petri Nets, Model Checking, Run time Verification
In the past decades, software architecture research has mainly concentrate on the conceptual construction and the development of various architecture description languages. This area has matured enough and thus requires more em phasis on validation and verification techniques. Model checking provides an efficient way to validate the model of systems automatically. Moreover, verification and vali dation of system designs on-the-fly continue to be a major challenge today. Runtime monitoring technique confirms that a system is satisfying the specification of system prop erties on a single trace so far. Based on these observation, in this paper, we propose an integrated framework to ver ify the software architecture through combining the run time monitoring and model checking technique together and applying this framework on the model of the system design by mapping the model to the implementation level. In addition, our framework provides the analysis ability on the high level behavior of the system model through model checking. After that, the prototype implementation of this framework on an architecture description language, SAM, is demonstrated. Finally, a non-trivial experiment result shows that this prototype implementation works well.
Important Links:
Go Back
