Enhancing the adoption of formal methods to design real-time systems

Abstract

Formal methods are being increasingly used in engineering industrial software. They are moatly used for specifying and verifying software requirements, but seldom in later development phases. This paper tries to bridge the gap between formal requirements specifiction and final code by introducing a formally defill ed désign notatlon. The propased design notation extends strtictured analysis specification notationswith conatructs derived from POSIX real-time extensions. The design notation proposed in this anide is formally defined. Also; an operational semantic la given by meana of high-Ievel timed Petri neta, and can be formally analyzed using tools and techniques available for Petri nets.