A Practical Formal Approach for Requirements Validation and Verification of Dependable Systems

Classical requirements validation methods usually work with static behavioral models, and under the assumption that there are no dependencies and interactions between the requirements. Requirements verification is mostly done by statically analyzing the design artifacts and by running tests. This work presents a practical formal approach for requirements validation and verification (V&V) of dependable systems, under two different perspectives: development and acquisition. The approach considers the system´s dynamic behavior that is formally represented as state chart assertions and validated using JUnit test scenarios. Runtime execution monitoring (REM) data is used to create JUnit tests to verify the system´s behavior against the assertions. The V&V activities are supported by the State Rover tool. Two space systems case studies are briefly presented. As dependability often manifests as decidable system sequencing behaviors, the main contribution of this work is centered on the validation and verification of such behaviors.