Integrating informal and formal approaches to requirements modeling and analysis
Betty H. C. Cheng, Laura A. Campbell · 2002
The Unified Modeling Language (UML) comprises several different notations for object-oriented modeling with no formal semantics attached to the individual diagrams. We have developed a generic framework for formalizing a subset of UML diagrams in terms of various formal languages, with a focus on embedded systems. We have formalized UML in terms of Promela, thus enabling analysis of the UML diagrams by the SPIN model checker and simulator. We have also developed a number of visualizations to assist in the interpretation of the analysis results. This paper presents a case study of the UML design and automated analysis of an industrial automotive embedded system using our formalization techniques, supporting tools and existing analysis.