Abstract
The Autonomic System Specification Language (ASSL) is a formal method dedicated to autonomic computing, and as such, assists developers with formal specification, validation and code generation of autonomic systems. Due to the synthesis approach of automatic code generation, ASSL guarantees consistency between a specification and the corresponding implementation. Moreover, one of the major objectives of the framework is to assure the correctness of autonomic systems via the inclusion of tools targeting model checking. In this paper, we report our experience in developing model-checking mechanisms for ASSL.
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
Vassev, E.: Towards a Framework for Specification and Code Generation of Autonomic Systems. PhD Thesis, Computer Science and Software Engineering Department, Concordia University, Quebec, Canada (2008)
Vassev, E.: ASSL: Autonomic System Specification Language - A Framework for Specification and Code Generation of Autonomic Systems. LAP Lambert Academic Publishing (2009)
Murch, R.: Autonomic Computing: On Demand Series. IBM Press (2004)
Vassev, E., Hinchey, M., Quigley, A.: Model Checking for Autonomic Systems Specified with ASSL. In: Proceedings of the First NASA Formal Methods Symposium (NFM 2009), NASA, pp. 16–25 (2009)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)
Bakera, M., Renner, C.: GEAR - Game-based, Easy and Reverse Model Checking (2008), http://jabc.cs.tu-dortmund.de/modelchecking/
Bakera, M., Wagner, C., Margaria, T., Vassev, E., Hinchey, M., Steffen, B.: Component-oriented Behavior Extraction for Autonomic System Design. In: Proceedings of the First NASA Formal Methods Symposium (NFM 2009), NASA, pp. 66–75 (2009)
Nagel, R.: jABC, http://www.jabc.de
Vassev, E., Hinchey, M.: Modeling the Image-processing Behavior of the NASA Voyager Mission with ASSL. In: Proceedings of the Third IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2009), pp. 246–253. IEEE Computer Society, Los Alamitos (2009)
Kozen, D.: Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982)
Java PathFinder, http://javapathfinder.sourceforge.net/
Visser, W., Havelund, K., Brat, G., Park, S.-J.: Model Checking Programs. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE 2000). IEEE Computer Society, Los Alamitos (2000)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vassev, E., Hinchey, M. (2011). Developing Model-Checking Mechanisms for ASSL: An Experience Report. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)