Abstract
We present the modeling and validation experiments performed with the IFx validation toolset and with the UML profile developed within the IST Omega project, on a representative space vehicle control system: a model of the Ariane-5 flight software obtained by manual reverse engineering. The goal of the study is to verify functional and scheduling-related requirements under different task architecture assumptions. The study is also a proof of concept for the UML-based validation technique proposed in IFx.
This work has been partially financed by the OMEGA IST project.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-34895-5_20
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arons, T., Hooman, J., Kugler, H., Pnueli, A., van der Zwaag, M.: Deductive verification of UML models in TLPVS. In: Baar, T., Strohmeier, A., Moreira, A., Mellor, S.J. (eds.) UML 2004. LNCS, vol. 3273, pp. 335–349. Springer, Heidelberg (2004)
Bianco, V.D., Lavazza, L., Mauri, M.: Model checking UML specifications of real time software. In: Proceedings of 8th International Conference on Engineering of Complex Computer Systems, IEEE, Los Alamitos (2002)
Bozga, M., Lesens, D., Mounier, L.: Model-Checking Ariane-5 Flight Program. In: Proceedings of FMICS 2001, Paris, France, Inria, pp. 211–227 (2001)
Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In: SFM-2004:RT 4th Int. School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, June 2004. LNCS (2004)
Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: A formal semantics of concurrency and communication in real-time UML. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, Springer, Heidelberg (2003)
David, A., Möller, O., Yi, W.: Formal verification UML statecharts with real time extensions. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, Springer, Heidelberg (2002)
del Mar Gallardo, M., Merino, P., Pimentel, E.: Debugging UML designs with model checking. Journal of Object Technology 1(2), 101–117 (2002)
Fernandez, J.-C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP - a protocol validation and verification toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis using two clocks. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, Springer, Heidelberg (2003)
Graf, S., Ober, I., Ober, I.: Timed annotations in UML. Int. Journal on Software Tools for Technology Transfer, Springer, Heidelberg (in print, 2006) , Available on Springer On-line at: http://dx.doi.org/10.1007/s10009-005-0219-x
Har’El, Z., Kurshan, R.P.: Software for Analysis of Coordination. In: Conference on System Science Engineering, Pergamon Press, Oxford (1988)
Holzmann, G.J.: The model-checker SPIN. IEEE Trans. on Software Engineering 23(5) (1999)
Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, Springer, Heidelberg (2002)
Larsen, K.G., Petterson, P., Yi, W.: UPPAAL: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 456–459. Springer, Heidelberg (1997)
Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioral subset of UML statechart diagrams using the SPiN model-checker. Formal Aspects of Computing (11) (1999)
Lilius, J., Paltor, I.P.: Formalizing UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, Springer, Heidelberg (1999)
Liu, C.L., Leyland, J.W.: Scheduling algorithms for multiprogramming in a hard real-time environment. JACM 20(1), 46–61 (1973)
Ober, I., Graf, S., Ober, I.: Validating timed UML models by simulation and verification. Int. Journal on Software Tools for Technology Transfer, Springer, Heidelberg (in print, 2006), Available on Springer On-line at: http://dx.doi.org/10.1007/s10009-005-0205-x
SysML Partners. SysML specification v. 0.9 draft (10 jan. 2005), Available at: http://www.sysml.org/artifacts.htm
Potop-Butucaru, D., Caillaud, B., Benveniste, A.: Concurrency in synchronous systems. In: Formal Methods in System Design 2005. LNCS, Springer, Heidelberg (2005)
Xie, F., Levin, V., Browne, J.C.: Model checking for an executable subset of UML. In: Proceedings of 16th IEEE International Conference on Automated Software Engineering (ASE 2001), IEEE, Los Alamitos (2001)
Yovine, S.: Kronos: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer 1(1-2) (December 1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Ober, I., Graf, S., Lesens, D. (2006). Modeling and Validation of a Software Architecture for the Ariane-5 Launcher. In: Gorrieri, R., Wehrheim, H. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2006. Lecture Notes in Computer Science, vol 4037. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11768869_6
Download citation
DOI: https://doi.org/10.1007/11768869_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34893-1
Online ISBN: 978-3-540-34895-5
eBook Packages: Computer ScienceComputer Science (R0)