Development of software for electronic systems in the aviation industry is strongly regulated by pre-defined standards. The aviation industry spends significant costs of development in ensuring flight safety and showing conformance to these standards. Some safety requirements can be satisfied by performing formal verification. Formal verification is seen as a way to reduce costs of showing conformance of software with the requirements or formal specifications. Therefore, the correctness of formal specifications is critical.
Writing formal specifications is at least as difficult as developing software [36]. This work proposes an approach to generate formal specifications from example data. This example data illustrates the natural language requirements and represents the ground truth about the system. This work eases the task of an engineer who has to write formal specifications by allowing the engineer to specify the example data instead. The use of a relationship model and a marking syntax and semantics are proposed that make the creation of formal specifications goal oriented. The evaluation of the approach shows that the proposed syntax and semantics capture more information than is strictly needed to generate formal specifications. The relationship model reduces the computational load and only produces formal specifications that are interesting for the engineer.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:72325 |
| Date | 02 October 2020 |
| Creators | Gulati, Pranav |
| Contributors | Hardt, Wolfram, Reich, Marina, Technische Universität Chemnitz |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, doc-type:masterThesis, info:eu-repo/semantics/masterThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0021 seconds