Abstract
This paper illustrates a technique to automatically derive intra-object behaviours (in the form of state diagrams) from an object model. We demonstrate how we may take specifications, written in a restricted language of pre- and postconditions, and generate protocols of usage that represent possible behaviours of the generated program. We discuss how to use these state diagrams to analyse the specification for errors, and how to produce correct abstractions to show a particular class of properties of a system. This approach proves successful and scalable for specific domains of application such as database systems and e-commerce websites.
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
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Davies, J., Crichton, C., Crichton, E., Neilson, D., Sørensen, I.H.: Formality, evolution, and model-driven software engineering. In: Mota, A., Moura, A. (eds.) Proceedings of SBMF 2004. ENTCS (2005)
Davies, J., Faitelson, D., Welch, J.: Domain-specific Semantics and Data Refinement of Object Models. In: Moreira, A.M., Ribeiro, L. (eds.) SBMF 2006: Brazilian Symposium on Formal Methods, pp. 185–200 (2006)
Davies, J., Welch, J., Cavarra, A., Crichton, E.: On the generation of object databases using booster. In: ICECCS 2006: Proceedings of the 11th IEEE International Conference on Engineering of Complex Computer Systems, Washington, DC, USA, pp. 249–258. IEEE Computer Society, Los Alamitos (2006)
Faitelson, D., Welch, J., Davies, J.: From predicates to programs: the semantics of a method language. Electronic Notes in Theoretical Computer Science (2006) (to appear)
Graham, I.: Graham/SOMA (Semantic Object Modeling Approach) method, pp. 73–83. Wiley-QED Publishing, Somerset, NJ (1994)
Gupta, A.: Automated Object’s Statechart Generation from Class Method Contract. In: Proceedings of the 3rd Workshop on Model design and Validation (MoDeV2a 2006): Perspectives on Integrating MDA and V&V, Genoa, Italy, October 2006, ACM/IEEE, New York (2006)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Heimdahl, M.P.E., Whalen, M.W.: Reduction and slicing of hierarchical state machines. In: Jazayeri, M., Schauer, H. (eds.) FSE 1997. LNCS, vol. 1267, pp. 450–467. Springer, Heidelberg (1997)
Holt, N.E., Anda, B.C.D., Asskildt, K., Briand, L.C.L., Endresen, J., FrØystein, S.: Experiences with precise state modeling in an industrial safety critical system. In: Houmb, S.H., Georg, G., France, R., Petriu, D.C., Jürjens, J. (eds.) Critical Systems Development Using Modeling Lanuguages, CSDUML 2006, pp. 68–77. Springer, Heidelberg (2006)
Kleppe, A., Warmer, J., Bast, W.: MDA Explained. The Model Driven Architecture: Practice and Promise. Addison-Wesley, Reading, MA (2003)
Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Commun. ACM 14(3) (1971)
Nowack, A.: Slicing abstract state machines. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 186–201. Springer, Heidelberg (2004)
Object Management Group. UML 2.0 superstructure specification (2005), http://www.omg.org/cgi-bin/doc?ptc/05-07-04
Prywes, N., Amir, S., Shastry, S.: Use of a nonprocedural specification language and associated program generator in software development. ACM Trans. Program. Lang. Syst. 1(2) (1979)
Ruth, G.R.: Automatic programming: Automating the software system development process. In: ACM 1977: Proceedings of the 1977 annual conference, ACM Press, New York (1977)
Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA, 2nd edn. Addison Wesley, Reading, MA (2003)
Welch, J., Faitelson, D., Davies, J.: Automatic maintenance of association invariants. In: SEFM 2005: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, pp. 282–292. IEEE Computer Society, Los Alamitos (2005)
Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: ICSE 2000: Proceedings of the 22nd international conference on Software engineering, New York, pp. 314–323. ACM Press, New York (2000)
Xie, T., Notkin, D.: Automatic extraction of sliced object state machines for component interfaces. In: Proceedings of the 3rd Workshop on Specification and Verification of Component-Based Systems at ACM SIGSOFT 2004/FSE-12 (SAVCBS 2004), pp. 39–46 (October 2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cavarra, A., Welch, J. (2007). Behavioural Specifications from Class Models. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)