Integrating Structural Design and Formal Methods in RealTime System Design

Formal methods have been advocated as one of those techniques that can produce highquality software and hardware systems that has been demonstrated to come in ontime, within budget, and satisfy procurer requirements. They are, however, perceived to be difficult to use and unsuitable for presentation to nonspecialists. In addition, they have been criticized for paying too little attention to the system development process.

Traditional structured ( bubblesandarrows ) methods, however, do excel at supporting the development process, but do not support proof of properties, etc.

Method integration offers a promising compromise. Such an approach exploits the benefits of both structured and formal methods, preserving an intuitive graphical notation and the ability to prove properties. The approach is of particular benefit in the area of realtime systems. We illustate the integration of a popular structured development method (JSD), which is assigned a formal semantics in terms of a variant of CSP, augmented with TLZ, itself a hybrid of Z and TLA, which addresses statebased aspects. The formalization suggests modifications to JSD which make it particularly suitable for use with realtime systems