A formal requirements engineering method for specification, synthesis, and verification

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 State-charts 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.