Formalisation of SysML Models and Analysis based on Refinement
Lucas Lima
- 320 páginas
- English
- PDF
- Disponible en iOS y Android
Formalisation of SysML Models and Analysis based on Refinement
Lucas Lima
Información del libro
The increasing complexity of systems has led to increasing difficulty in design. For critical systems, for which safety is a major concern, early verification and validation (V&V) is recognised as a valuable approach to promote dependability. We address these issues with a refinement technique for SysML supported by tools. In this work we describe our semantics for SysML, which is defined using a state-rich process algebra called CML and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case studies are a leadership-election protocol, a critical component of an industrial application, and a dwarf signal, a device used to control rail traffic. Our contributions are: a set of guidelines that provide meaning to the different modelling elements of SysML used during the design of systems; the individual formal semantics for SysML activities, blocks and interactions; an integrated semantics that combines these semantics with another defined for state machines; and a framework for reasoning using refinement about systems specified by collections of SysML diagrams.