Towards a Formal Approach to Validating and Verifying Functional Design for Complex Safety Critical Systems

Abstract

The quality and reliability of safety critical
software systems are highly dependent on proper system
validation and verification. In model-driven software
development, semi-formal notations are often used in
requirements capture. Though semi-formal notations possess
advantages, their major disadvantage is their imprecision. A
technique to eliminate imprecision is to transform semi-formal
models into an analyzable representation using formal
specification techniques (FSTs). With this approach to system
validation and verification, safety critical systems can be
developed more reliably. This work documents early experience
of applying FSTs on UML class diagrams as attribute
constraints, and pre- post-conditions on procedures. The
validation and verification of the requirements of a system to
monitor unmanned aerial vehicles in unrestricted airspace is the
origin of this work. The challenge is the development of a system
with incomplete specifications; multiple conflicting stakeholders’
interests; existence of a prototype system; the need for
standardized compliance, where validation and verification are
paramount, which necessitates forward and reverse engineering
activities.