2004 | OriginalPaper | Buchkapitel
Formal Verification of LSCs in the Development Process
verfasst von : Matthias Brill, Ralf Buschermöhle, Werner Damm, Jochen Klose, Bernd Westphal, Hartmut Wittke
Erschienen in: Integration of Software Specification Techniques for Applications in Engineering
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper presents how a model-based development process can be enhanced by the combination of using Live Sequence Charts (LSC) as the formal language to describe interactions together with automatic formal verification techniques that decide whether communication sequences are exhibitable or adhered to by the system. We exemplify our approach on the V-model, a widely used development process, considering a (Statemate) statecharts design of the reference case study “Funkfahrbetrieb” (FFB) and discuss potential assets and drawbacks. We sketch a set of best practices on the use of LSC features and emphasise the possibilities for re-use of LSCs in the different activities of the development process. To give evidence for feasibility of automatic formal verification of LSCs, as well as its limitations, we present our approaches to the verification of possible and mandatory LSC requirements on Statemate models. We report experimental results we have obtained from formal verification of the FFB and briefly discuss the treatment of Statemate’s different notions of time.