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, 1 (2). 167-191. ISSN 0928-8910
|
(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.
Repository Staff Only: item control page