Abstract
The specification of software for distributed production control systems is an error prone task. The ISILEIT project aims at the development of a seamless methodology for the integrated design, analysis and validation of such embedded systems. Suitable subsets of UML and SDL for the design of such systems are therefore identified in a first step. The paper then focuses on how we use a series of formal semantics of our design language to enable the effective evaluation of software designs by means of validation and verification. We will further explain how the use of multiple Abstract State Machine meta-models permits simulation and model checking at different levels of abstraction
This work has been supported by the German Research Foundation (SPP1064,GA 456/7).
The updated original online version for this book can be found at DOI: 10.1007/978-0-387-35599-3_29
Chapter PDF
Similar content being viewed by others
Key words
References
Integrative Specification of Distributed Control Systems for the Flexible Automated Manufacturing (ISILEIT), German Research Foundation (DFG) program “integrative specification of engineering applications”.: http://www.upb.de/cs/isileit/
Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading, Massachusetts, 1999.
ITU-T Recommendation Z.100, Specification and Description Language (SDL), International Telecommunication Union (ITU), Geneva, 1994 + Addendum 1996.
H.J. Köhler, U. Nickel, J. Niere, and A. Ztlndorf. Integrating UML Diagrams for Production Control Systems. In Proc. of the 22th Int. Conf. on Software Engineering (ICSE), Limerick, Irland. ACM Press, 2000.
Y. Gurevich: Evolving Algebras 1993: Lipari Guide; E. Borger (Eds.): Specification and Validation Methods; Oxford University Press, 1995.
R. Eschbach, U. Glasser, R. Gotzhein, M. von Löwis and A. Prinz: Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models. Journal of Universal Computer Science ( J.UCS ), October 2001.
G. del Castillo and K. Winter: Model checking support for the ASM high-level language. In S. Graf and M. Schwartzbach, editors, Proc. on 6th Int. Conf. TACAS 2000, volume 1785 of LNCS, pages 331–346, 2000.
H. Giese, M. Kardos and U. Nickel: Integrating Verification in a Design Process for Distributed Production Control Systems. Second International Workshop on Integration of Specification Techniques for Applications in Engineering (INT 2002). Grenoble, France, April 2002. (to appear)
http://www.research.microsoft.com/fse/AsmL/default.html
James D. Arthur, Markus K. G“oner, Kelly I. Hayhurst, and C. Michael Holloway. Evaluating the Effectiveness of Independent Verification and Validation. IEEE Computer, 32 (10): 79–83, October 1999.
U. Nickel and J. Niere, ‘Modelling and Simulation of a Material Flow System’, in Proc. of Workshop ‘Modellierung’ (Mod), Bad Lippspringe, Germany, Gesellschaft für Informatik, 2001.
William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon D. Reese. Model Checking Large Software Specifications. IEEE Transactions on Software Engineering, 24 (7): 498–520, 1998.
M. Bozga, J.C1. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, J. Sifakis. IF: An Intermediate Representation for SDL and its Applications. Proceedings of SDLFORUM 1999 ( Montreal, Canada ) June 1999.
Gihwon Kwon. Rewrite Rules and Operational Semantics for Model Checking UML Statecharts. In Andy Evans, Stuart Kent, and Bran Selic, editors, Proceedings of the third International Conference on the Unified Modeling Language (UML 2000), York, UK, volume 1939, page 528ff. Springer Verlag, October 2000.
Johan Lilius and Ivan Pones Paltor. vUML: a Tool for Verifying UML Models. In Proceedings of the 14th IEEE International Conference on Automated Software Engineering, Cocoa Beach, Florida, USA, 1999.
Prasanta Bose. Automated Translation of UML Models of Architectures for Verification and Simulation Using SPIN. In Proceedings of the 14th IEEE International Conference on Automated Software Engineering, Cocoa Beach, Florida, USA, 1999.
http://www-omega.imag.frI.
D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Tauring, and M. Trakhtenbrot. STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Trans. Soft. Eng., 16, 403–414, 1990, Paderborn, 1999.
A. Scharr, A. J. Winter, A. Zündorf. Graph grammar engineering with PROGRES. In W. Schäfer, Editor, Software Engineering - ESEC ‘85, LNCS 989, Springer Verlag, 1995.
Telelogic Tau SDL Suite: http://www.telelogic.com
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Giese, H., Kardos, M., Nickel, U. (2002). Towards Design Verification and Validation at Multiple Levels of Abstraction. In: Kleinjohann, B., Kim, K.H., Kleinjohann, L., Rettberg, A. (eds) Design and Analysis of Distributed Embedded Systems. DIPES 2002. IFIP — The International Federation for Information Processing, vol 91. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35599-3_8
Download citation
DOI: https://doi.org/10.1007/978-0-387-35599-3_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-4937-3
Online ISBN: 978-0-387-35599-3
eBook Packages: Springer Book Archive