OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Verifying service continuity in a satellite reconfiguration procedure: application to a satellite

Apvrille, Ludovic and Saqui-Sannes, Pierre de and Sénac, Patrick and Lohr, Christophe Verifying service continuity in a satellite reconfiguration procedure: application to a satellite. (2004) Automated Software Engineering, vol. 1 (n° 2). pp. 167-191. ISSN 0928-8910

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
584kB

Official URL: http://dx.doi.org/10.1023/B:AUSE.0000017742.47984.6c

Abstract

The paper discusses the use of the TURTLE UML profile to model and verify service continuity during dynamic reconfiguration of embedded software, and space-based telecommunication software in particular. TURTLE extends UML class diagrams with composition operators, and activity diagrams with temporal operators. Translating TURTLE to the formal description technique RT-LOTOS gives the profile a formal semantics and makes it possible to reuse verification techniques implemented by the RTL, the RT-LOTOS toolkit developed at LAAS-CNRS. The paper proposes a modeling and formal validation methodology based on TURTLE and RTL, and discusses its application to a payload software application in charge of an embedded packet switch. The paper demonstrates the benefits of using TURTLE to prove service continuity for dynamic reconfiguration of embedded software.

Item Type:Article
Additional Information:Thanks to Springer editor. The definitive version is available at http://www.springerlink.com The original PDF of the article can be found at Automated Software Engineering website: http://www.springerlink.com/content/100242/
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE
Other partners > Concordia University (CANADA)
Other partners > Telecom ParisTech (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS
Laboratory name:
Statistics:download
Deposited By: Pierre de Saqui-Sannes

Repository Staff Only: item control page