In: Proc. 3-rd Int. IEEE High-Assurance Systems Engineering Symposium, 13-14 November 1998, Washington, DC, pages 270-278. 1998.
Also in: Annals of Software Engineering, Vol. 7, No. 1, pages 47-70. 1999.
Abstract: A real-time architectural specification (RAS) approach and its application to command and control (C2) systems is presented. The objective is to establish a formal foundation that will enable us to integrate existing rich but fragmented formal techniques for system specification and verification into practical and scalable formal engineering methods to support the design and development of highly reliable real-time distributed systems. RAS is built on top of time Petri nets and real-time computational tree logic (RTCTL). The contribution of RAS is twofold. First, it provides a formal system that integrates system's timing requirements and the propagation of requirements into the process of architectural modeling and design and provides a systematic way to enforce that the requirements are met at every step of the design process. Second, it offers an incremental and more scalable to design modeling. These two features together make RAS a suitable model for the design of C2 systems. Based on these features, an incremental method is presented for verifying timing properties of a RAS model that helps to reduce the complexity of analysis both at a given design level or across different design levels.
Keywords: RAF, RTCTL, command and control systems, computational tree logic, formal methods, real-time systems, software architecture, time Petri nets.
Back to the Petri Nets Bibliography