Abstract
The complexity of middleware leads to complex Application Programming Interfaces (APIs) and semantics, supported by configurable components in the middleware. Those components are selected to provide the desired semantics. Yet, incorrect configuration can lead to faulty middleware executions, detected late in the development cycle.
We use formals methods to tackle this problem. They allow us to find appropriate composition of middleware components and the use of their APIs, and to detect valid or faulty sequences. To provide reusable results, we modeled a canonical middleware architecture using Z.
We propose a validation scenario to verify middleware’s invariants. We define invariants to exhibit inconsistent usage of these APIs. The specification has been checked with the Z/EVES [13] theorem prover.
This work is funded in part by the ANR/RNTL Flex-eWare project.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Basin, D., Rittinger, F., Viganò, L.: A Formal Analysis of the CORBA Security Service. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 330–349. Springer, Heidelberg (2002)
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14(1), 25–59 (1987)
Freitas, L.: Posix 1003.21 standard – real time distributed systems communication (in Z/Eves). Technical report, University of York (2006)
Object Management Group. Corba component model 4.0 specification. Specification Version 4.0, Object Management Group (April 2006)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 26(1), 53–56 (1983)
Hugues, J., Thierry-Mieg, Y., Kordon, F., Pautet, L., Baarir, S., Vergnaud, T.: On the Formal Verification of Middleware Behavioral Properties. In: Proceedings of the 9th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004), Linz, Austria (September 2004)
Kreuz, D.: Formal specification of corba services using object-z. In: ICFEM 1998: Proceedings of the Second IEEE International Conference on Formal Engineering Methods, Washington, DC, USA, p. 180. IEEE Computer Society Press, Los Alamitos (1998)
Milnes, B., Pelton, G., Doorenbos, R., Laird, M., Rosenbloom, P., Newell, A.: A specification of the soar cognitive architecture in z. Technical report, Pittsburgh, PA, USA (1992)
OMG. OCL 2.0 Specification - Version 2.0 ptc/2005-06-06. OMG (June 2005)
Raman, K., Zhang, Y., Panahi, M., Colmenares, J., Klefstad, R., Harmon, T.: Rtzen: Highly predictable, real-time java middleware for distributed and embedded systems (2005)
Rosa, N., Cunha, P.: A formal framework for middleware behavioural specification. SIGSOFT Softw. Eng. Notes 32(2), 1–7 (2007)
Schmidt, D.C., Levine, D.L., Mungee, S.: The design of the TAO real-time object request broker. Computer Communications 21(4), 294–324 (1998)
Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall, Inc., Upper Saddle River (1989)
Valk, R.: Basic definitions, ch. 4. In: Girault, C., Valk, R. (eds.) Petri nets and system engineering, 1st edn., pp. 41–51. Springer, Heidelberg (2003)
Vergnaud, T., Hugues, J., Pautet, L., Kordon, F.: PolyORB: a schizophrenic middleware to build versatile reliable distributed applications. In: Llamosí, A., Strohmeier, A. (eds.) Ada-Europe 2004. LNCS, vol. 3063, pp. 106–119. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Renault, X., Hugues, J., Kordon, F. (2008). Formal Modeling of a Generic Middleware to Ensure Invariant Properties. In: Barthe, G., de Boer, F.S. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2008. Lecture Notes in Computer Science, vol 5051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68863-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-68863-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68862-4
Online ISBN: 978-3-540-68863-1
eBook Packages: Computer ScienceComputer Science (R0)