Multi-Aspect System Analysis Using State Machines Extracted from Specifications in VDM–SL
Kengo Miyoshi, Satoru Hirachi, Shigeru Kusakabe, Keijiro Araki, 健吾 三好, 智 平地, 茂 日下部, 啓二郎 荒木 · QIR (Kyushu University Institutional Repository) (Kyushu University) · 2004
Model-oriented formal specification languages such as VDM-SL is useful to describe functional requirements of the target systems. However, since single-aspect analysis is not enough to make reliable specifications, we also use other approaches such as model checking to analyze dynamic aspects of the system as a part of multi-aspect analysis. In this paper, we discuss our approach to extract state machines from specifications in VDM-SL.We can analyze both static and dynamic aspect by using these two different kinds of specification languages, model-oriented and state-machine languages in an integrated manner.