| 000 -LEADER |
|---|
| fixed length control field |
a |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OSt |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20230103142159.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
230103b xxu||||| |||| 00| 0 eng d |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
AIKTC-KRRC |
| Transcribing agency |
AIKTC-KRRC |
| 100 ## - MAIN ENTRY--PERSONAL NAME |
|---|
| 9 (RLIN) |
19546 |
| Author |
Nallamalli, Ranjana . |
| 245 ## - TITLE STATEMENT |
|---|
| Title |
Novel Patterns for Formal Verification of System Safety Properties |
| 250 ## - EDITION STATEMENT |
|---|
| Volume, Issue number |
Vol, 103(6), Dec |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. |
|---|
| Place of publication, distribution, etc. |
New York |
| Name of publisher, distributor, etc. |
Springer |
| Year |
2022 |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Pagination |
2049–2056p |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
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. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| 9 (RLIN) |
4623 |
| Topical term or geographic name entry element |
Electrical Engineering |
| 700 ## - ADDED ENTRY--PERSONAL NAME |
|---|
| 9 (RLIN) |
19547 |
| Co-Author |
Chauhan, Durg Singh |
| 773 0# - HOST ITEM ENTRY |
|---|
| Title |
Journal of the institution of engineers (India): Series B |
| International Standard Serial Number |
2250-2106 |
| 856 ## - ELECTRONIC LOCATION AND ACCESS |
|---|
| URL |
https://link.springer.com/article/10.1007/s40031-022-00788-6 |
| Link text |
Click here |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Source of classification or shelving scheme |
|
| Koha item type |
Articles Abstract Database |
