Title :
Integrating informal and formal approaches to requirements modeling and analysis
Author :
Cheng, Betty H C ; Campbell, Laura A.
Author_Institution :
Dept. of Comput. Sci. & Eng., Michigan State Univ., East Lansing, MI, USA
Abstract :
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
Keywords :
diagrams; embedded systems; formal specification; formal verification; object-oriented methods; specification languages; Promela; SPIN model checker; UML diagrams; Unified Modeling Language; analysis results interpretation; automated analysis; case study; formal approaches; formal languages; formal semantics; industrial automotive embedded system; informal approaches; notations; object-oriented modeling; our formalization techniques; requirements analysis; requirements modeling; supporting tools; visualizations; Analytical models; Computer science; Embedded software; Embedded system; Formal languages; Laboratories; Object oriented modeling; Software engineering; Testing; Unified modeling language;
Conference_Titel :
Requirements Engineering, 2001. Proceedings. Fifth IEEE International Symposium on
Conference_Location :
Toronto, Ont.
Print_ISBN :
0-7695-1125-2
DOI :
10.1109/ISRE.2001.948591
