Enhancing the adoption of Formal Methods to Design Real Time Systems

VICTOR A. BRABERMAN; FABIO PIENIAZCK; MIGUEL FELDER

San Luís, Argentina

Congreso; Congreso Argentino de Ciencias de la Computación; 1996

CACIC

Formal methods are being increasingly used in engineering industrial software. They are mostly used for specifying and verifying software requirements, but seldom in later development phases. This report tries to bridge the gap between formal requirements specification and final code by introducing a formally defined design notation. The proposed design notation extends structured analysis specification notations with constructs derived from POSIX real-time extensions. The design notation proposed in this report is formally defined. Also, an operational semantic is given by means of high-level timed Petri nets, and can be formally analyzed using tools and techniques available for Petri nets. Automatic tools for editing and verifying design specifications given in terms of the notation proposed in this report have been implemented and the notation has been successfully validated on industrial case-studies.