Abstract
We present in this paper a rigorous and automated based approach for the behavioral validation of control software systems. This approach relies on metamodeling, model-transformations and process algebra and combines semi-formal object-oriented models with formal validation. We perform the validation of behavioral aspects of object-oriented models by using a projection into a well-defined formal technical space (Finite State Process algebra) where model-checkers are available (we use LTSA; a model checker for Labeled Transition Systems). We then target an implementation platform, which conforms to the semantics of the formal technical space; in turn, this ensure conformance of the final application to the validated specification.
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.
References
Sanz, R., Pfister, C., Schaufelberger, W., De Atonio, A.: Software for Complex Controllers. In: Astrom, K., Albertos, P., Blanke, M., Isidori, A., Schaufelberger, W., Sanz, R. (eds.) Control Of Complex Systems, pp. 143–164. Springer, London (2001)
Bézivin: search of a Basic Principle for Model-Driven Engineering. Novatica Journal, Special Issue (2004)
Magee, J., Kramer, J.: Concurrency State Models & Java Programs. John Wiley & Sons, Chichester (1999)
Arnold, A.: Finite Transition System. Prentice Hall, Englewood Cliffs (1994)
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier Science, Amsterdam (2001)
Thirion, B., Thiry, L.: Concurrent programming for the Control of Hexapode Walking. ACM Ada letters n°21, 12–36 (2002)
Lin, F., Wonham, W.M.: Decentralized Control and Coordination of Discrete-Event Systems with Partial Observation. IEEE Transactions on Automatic Control 35(12), 1330–1337 (1990)
Perronne, J.M., Rasse, A., Thiry, L., Thirion, B.: A Modeling Framework for Complex Behavior Modeling and Integration. In: Proceedings of IADIS 2005, Algrave, Portugal (2005)
Bérard, B., et al.: Systems and Software verification. In: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. The MIT Press, Cambridge (1999)
Domain Specific Modeling with MetaEdit+ (January 2005), http://www.metacase.com/
Rasse, A., Perronne, J., Thirion, B.: Toward a Validated Object-Oriented Design Approach to Control Software. In: Proceedings of 16th IFAC World Congress, Prague, Czech Republic (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rasse, A., Perronne, JM., Muller, PA., Thirion, B. (2006). Using Process Algebra to Validate Behavioral Aspects of Object-Oriented Models. In: Bruel, JM. (eds) Satellite Events at the MoDELS 2005 Conference. MODELS 2005. Lecture Notes in Computer Science, vol 3844. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11663430_5
Download citation
DOI: https://doi.org/10.1007/11663430_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31780-7
Online ISBN: 978-3-540-31781-4
eBook Packages: Computer ScienceComputer Science (R0)