Novel Patterns for Formal Verification of System Safety Properties
By: Nallamalli, Ranjana
.
Contributor(s): Chauhan, Durg Singh.
Publisher: New York Springer 2022Edition: Vol, 103(6), Dec.Description: 2049–2056p.Subject(s): Electrical EngineeringOnline resources: Click here
In:
Journal of the institution of engineers (India): Series BSummary: Single-shot operation systems like missiles and satellite launch vehicles operate on pre-defined sequence of control with built-in safety constraints. Safety parameters and their specifications are defined during the system engineering process. An objective of early validation requires that system safety aspects be verified during the phase of software requirements analysis. Formal verification during requirements engineering phase can ensure the validity and consistency of functionality with respect to safety constraints. Predicates and existing patterns of formal properties representing absence, universality, existence, bounded existence, response and their popular derivatives are not sufficient to correctly represent the properties for the operational zones of single-shot safety critical systems. It is proposed a new class of patterns for enumerating system safety properties to be validated during the software requirements analysis for safety critical single-shot system. This ensures that operations occur based on specific safe zones but do not occur outside these. The new system property patterns are evaluated for single-shot mission controller system software module using a formal model. Modelling framework AutoFOCUS3 and a state-of-the-art formal verification engine NuXMV are used to verify the Linear Temporal Logic-based system safety patterns.
| Item type | Current location | Call number | Status | Date due | Barcode | Item holds |
|---|---|---|---|---|---|---|
Articles Abstract Database
|
School of Engineering & Technology Archieval Section | Not for loan | 2023-0018 |
Single-shot operation systems like missiles and satellite launch vehicles operate on pre-defined sequence of control with built-in safety constraints. Safety parameters and their specifications are defined during the system engineering process. An objective of early validation requires that system safety aspects be verified during the phase of software requirements analysis. Formal verification during requirements engineering phase can ensure the validity and consistency of functionality with respect to safety constraints. Predicates and existing patterns of formal properties representing absence, universality, existence, bounded existence, response and their popular derivatives are not sufficient to correctly represent the properties for the operational zones of single-shot safety critical systems. It is proposed a new class of patterns for enumerating system safety properties to be validated during the software requirements analysis for safety critical single-shot system. This ensures that operations occur based on specific safe zones but do not occur outside these. The new system property patterns are evaluated for single-shot mission controller system software module using a formal model. Modelling framework AutoFOCUS3 and a state-of-the-art formal verification engine NuXMV are used to verify the Linear Temporal Logic-based system safety patterns.
Click on an image to view it in the image viewer
There are no comments for this item.