Formal Requirements Specification for Command and Control Systems

Jaco van de Pol, Jozef Hooman and Edwin de Jong

Appeared in: Proceedings of the Conference on Engineering of Computer Based Systems, IEEE, pages 37-44, 1998.


This paper presents an approach to formal requirements specification of embedded systems. The specific demands of a specification for command and control systems are addressed. The proposed method allows various views of a system, like conventional methods. The added value lies in the fact that the relationship between the views is specified formally, and consistency between views can be analyzed formally. As a case study, we develop and analyze a formal requirements specification for a subsystem of a realistic command and control system. Specification and verification are carried out using the language and proof checker of PVS.