Abstract
This paper presents a formal requirements engineering method capturing specification, synthesis, and verification. Being multi-paradigm, our approach integrates individual established formal methods: temporal logics are used to express abstract specifications in the form of loose global constraints, like ordering requirements, or abstract safety and liveness properties, whereas Statecharts are used to support the development of a detailed, hierarchical specification at the concrete level. The link between these two specification layers is established by means of 1) a semi-automatic synthesis procedure, where sequential portions of Statecharts, automatically synthesized from abstract specifications, can be manually composed into structured Statecharts, and 2) by automatic formal verification via model checking, which validates the global constraints for the resulting overall Statechart specification. The method is illustrated along a detailed user session.
| Original language | English |
|---|---|
| Pages | 131-144 |
| Number of pages | 14 |
| Publication status | Published - 1997 |
| Externally published | Yes |
| Event | Proceedings of the 1997 8th Conference on Software Engineering Environments, SEE 97 - Cottbus, Ger Duration: 8 Apr 1997 → 9 Apr 1997 |
Conference
| Conference | Proceedings of the 1997 8th Conference on Software Engineering Environments, SEE 97 |
|---|---|
| City | Cottbus, Ger |
| Period | 8/04/97 → 9/04/97 |