Alapide et al 2013a - Revision history

Scipediacontent at 13:56, 21 January 2021

2021-01-21T13:56:38Z

Scipediacontent: Scipediacontent moved page Draft Content 493318396 to Alapide et al 2013a

2020-10-14T14:04:40Z

Scipediacontent moved page Draft Content 493318396 to Alapide et al 2013a

Scipediacontent: 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..."

2020-10-14T14:04:37Z

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..."

New page

== 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.

Document type: Part of book or chapter of book

== Full document ==
<pdf>Media:Draft_Content_493318396-beopen929-5371-document.pdf</pdf>

== Original document ==

The different versions of the original document can be found in:

* [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]

← Older revision		Revision as of 13:56, 21 January 2021
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.
−
−	~~Document type: Part of book or chapter of book~~
−
−	~~== Full document ==~~
−	~~<pdf>Media:Draft_Content_493318396-beopen929-5371-document.pdf</pdf>~~


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]

← Older revision	Revision as of 14:04, 14 October 2020
(No difference)