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

DOI: 10.5176/2251-2217_SEA43

Authors: Emanuel S. Grant, Vanessa K. Jackson, and Sophine A. Clachar

Abstract:

System validation and verification are fundamental to assuring quality and reliability of safety critical systems. In model-driven software development, semi-formal notations are often used in requirements capture. Semi-formal notations possess advantages, but are imprecise. A technique to eliminate imprecision is transforming semi-formal models into an analyzable representation using formal specification techniques (FSTs). Such an approach to system validation and verification is useful in developing safety critical systems. This work documents early experience of applying FSTs on UML class diagrams as attribute constraints, and pre- post-conditions on procedures. The genesis is with the validation and verification of requirements for a system to monitor unmanned aerial vehicles in unrestricted airspace. 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.

Keywords: model transformation; formal specification techniques; requirements engineering