(Created page with " == Abstract == This paper illustrates two different approaches for the application of Formal Methods (FM): integrated-parallel and after-the-fact. In the first approach FMs...") |
|||
| (One intermediate revision by the same user not shown) | |||
| Line 3: | Line 3: | ||
This paper illustrates two different approaches for the application of Formal Methods (FM): integrated-parallel and after-the-fact. In the first approach FMs have been applied integrated and in parallel with structured methods starting from the design phase. In the second approach FMs have been applied after the whole application code had already been developed, before the delivery, to derive an abstract specification of the S/W system and verifY that the most critical properties hold. Both approaches have been adopted in the development of a real application in the domain of the Air Traffic Control, whose purpose is to predict and detect potential air conflicts. The results show that FMs can improve the quality of the software process and products. In particular the accuracy of the final documentation improves and the number of early discovered errors increases. The paper provides general guidelines for the integration of formal and structured methods and presents the documentation outline which has been defined to comment the formal specifications, in the framework of the project applicable standards: 2I67-A military standard and ESA PSS-05-0 and PSS-OI-O. Finally the paper makes an analysis of eight software quality factors, showing also the typology of the discovered errors with the two after-the-fact and integrated-parallel approaches with respect to the traditional development approaches. One conclusion is that FMs provide a real support in developing better quality software, identifYing errors, which sometimes, with traditional approaches, remain undiscovered till and after the software delivery. | This paper illustrates two different approaches for the application of Formal Methods (FM): integrated-parallel and after-the-fact. In the first approach FMs have been applied integrated and in parallel with structured methods starting from the design phase. In the second approach FMs have been applied after the whole application code had already been developed, before the delivery, to derive an abstract specification of the S/W system and verifY that the most critical properties hold. Both approaches have been adopted in the development of a real application in the domain of the Air Traffic Control, whose purpose is to predict and detect potential air conflicts. The results show that FMs can improve the quality of the software process and products. In particular the accuracy of the final documentation improves and the number of early discovered errors increases. The paper provides general guidelines for the integration of formal and structured methods and presents the documentation outline which has been defined to comment the formal specifications, in the framework of the project applicable standards: 2I67-A military standard and ESA PSS-05-0 and PSS-OI-O. Finally the paper makes an analysis of eight software quality factors, showing also the typology of the discovered errors with the two after-the-fact and integrated-parallel approaches with respect to the traditional development approaches. One conclusion is that FMs provide a real support in developing better quality software, identifYing errors, which sometimes, with traditional approaches, remain undiscovered till and after the software delivery. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| Line 15: | Line 10: | ||
* [https://link.springer.com/content/pdf/10.1007%2F978-0-387-34869-8_27.pdf https://link.springer.com/content/pdf/10.1007%2F978-0-387-34869-8_27.pdf] | * [https://link.springer.com/content/pdf/10.1007%2F978-0-387-34869-8_27.pdf https://link.springer.com/content/pdf/10.1007%2F978-0-387-34869-8_27.pdf] | ||
| + | |||
| + | * [http://link.springer.com/content/pdf/10.1007/978-0-387-34869-8_27 http://link.springer.com/content/pdf/10.1007/978-0-387-34869-8_27], | ||
| + | : [http://dx.doi.org/10.1007/978-0-387-34869-8_27 http://dx.doi.org/10.1007/978-0-387-34869-8_27] | ||
| + | |||
| + | * [https://link.springer.com/chapter/10.1007/978-0-387-34869-8_27 https://link.springer.com/chapter/10.1007/978-0-387-34869-8_27], | ||
| + | : [https://www.scipedia.com/public/Alapide_et_al_2013a https://www.scipedia.com/public/Alapide_et_al_2013a], | ||
| + | : [https://academic.microsoft.com/#/detail/2119741180 https://academic.microsoft.com/#/detail/2119741180] | ||
Latest revision as of 14:56, 21 January 2021
Abstract
This paper illustrates two different approaches for the application of Formal Methods (FM): integrated-parallel and after-the-fact. In the first approach FMs have been applied integrated and in parallel with structured methods starting from the design phase. In the second approach FMs have been applied after the whole application code had already been developed, before the delivery, to derive an abstract specification of the S/W system and verifY that the most critical properties hold. Both approaches have been adopted in the development of a real application in the domain of the Air Traffic Control, whose purpose is to predict and detect potential air conflicts. The results show that FMs can improve the quality of the software process and products. In particular the accuracy of the final documentation improves and the number of early discovered errors increases. The paper provides general guidelines for the integration of formal and structured methods and presents the documentation outline which has been defined to comment the formal specifications, in the framework of the project applicable standards: 2I67-A military standard and ESA PSS-05-0 and PSS-OI-O. Finally the paper makes an analysis of eight software quality factors, showing also the typology of the discovered errors with the two after-the-fact and integrated-parallel approaches with respect to the traditional development approaches. One conclusion is that FMs provide a real support in developing better quality software, identifYing errors, which sometimes, with traditional approaches, remain undiscovered till and after the software delivery.
Original document
The different versions of the original document can be found in:
Document information
Published on 01/01/2013
Volume 2013, 2013
DOI: 10.1007/978-0-387-34869-8_27
Licence: CC BY-NC-SA license
Share this document
Keywords
claim authorship
Are you one of the authors of this document?