Abstract
This paper provides an overview on the approach of the Ist Omega project for the development of correct software for embedded systems based on the use of UML as modelling language. The main contributions of the project are the definition of a useful subset of UML and some extensions, a formal dynamic semantics integrating all notations and a tool set for the validation of models based on this semantics.
This work has been supported by the IST-2002-33522 OMEGA project – http://www-omega.imag.fr
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
ARTiSAN (2001)
Bienmüller, T., Damm, W., Wittke, H.: The STATEMATE Verification Environment – Making it real. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L.: IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, p. 307. Springer, Heidelberg (1999)
Clarke, E.M., Emerson, E.A., Sistla, E.: Automatic verification of finite state concurrent systems using temporal logic specification: a practical approach. In: ACM Symposium on Principles of Programming Languages, POPL (1983)
Compton, K., Huggins, J., Shen, W.: A semantic model for the state machine in the unified modelling language. In: Dynamic Behaviour in UML Models: Semantic Questions, UML 2000 Workshop (2000)
Damm, W., Harel, D.: LSCs: Breathing life into Message Sequence Charts. In: FMOODS 1999, Int. Conf. on Formal Methods for Open Object-Based Distributed Systems, Kluwer, Dordrecht (1999)
Damm, W., Josko, B., Pnueli, A., Votintseva, A.: A formal semantics for a UML kernel language. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W.-P. (eds.) 1st Symp. on Formal Methods for Components and Objects, revised lectures. LNCS Tutorials, vol. 2852 (2003)
Bozga, M., Graf, S., Mounier, L.: IF-2.0: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 343. Springer, Heidelberg (2002)
Harel, D.: Statecharts: A visual formalism for complex systems. Sci. Comput. Programming 8, 231–274 (1987)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out. In: Companion of the ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (2003)
Ilogix. Rhapsody development environment
Jensen, H., Larsen, K.G., Skou, A.: Scaling up UPPAAL:Automatic verification of real-time systems using compositionality and abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 19. Springer, Heidelberg (2000)
Kyas, M., de Boer, F.: D1.2.1: Assertion Languages for Object Structures in UML. Deliverable of the IST-2001-33522 OMEGA project (2002)
Kyas, M., de Boer, F.: On message specification in OCL. In: Compositional Verification in UML, Workshop associated with UML 2003 (2003)
Kyas, M., de Boer, F., Jacob, J., Zwaag, M.v.d.: Translating UML and OCL to PVS (2003) (submitted)
Lilus, J., Porres Paltor, I.: vUML: a tool for verifying UML models. Technical Report No 272, Turku Centre for Computer Science (1999)
Ober, I., Graf, S., Ober, I.: Model checking of UML models via a mapping to communicating extended timed automata. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 127–145. Springer, Heidelberg (2004)
OMG. Response to the OMG RFP for Schedulability, Performance and Time, v. 2.0. OMG document ad/2002-03-04 (March 2002)
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, Springer, Heidelberg (1982)
Shankar, N., Owre, S., Rushby, J.M.: The PVS proof checker: A reference manual (draft). Tech. report, Comp. Sci.,Laboratory, SRI International (1993)
Selic, B., Rumbaugh, J.: Using UML for Modeling Complex Real-Time Systems. Whitepaper, Rational Software Corp. (March 1998)
Telelogic. TAU Generation 2 Reference Manual (2002)
Zwaag, M.v.d., Hooman, J.: A semantics of communicating reactive objects with timing. In: Proc. ofWorkshop on Specification and Validation of UML models for Real-Time Embedded Systems, SVERTS (2003)
Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Reading (1998)
Yovine, S.: Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer 1(1-2) (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graf, S., Hooman, J. (2004). Correct Development of Embedded Systems. In: Oquendo, F., Warboys, B.C., Morrison, R. (eds) Software Architecture. EWSA 2004. Lecture Notes in Computer Science, vol 3047. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24769-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-24769-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22000-8
Online ISBN: 978-3-540-24769-2
eBook Packages: Springer Book Archive