Abstract
In this paper we present an action/state-based logical framework for the analysis and verification of complex systems, which relies on the definition of doubly labelled transition systems. The defined temporal logic, called UCTL, combines the action paradigm—classically used to describe systems using labelled transition systems—with predicates that are true over states—as captured when using Kripke structures as semantic model. An efficient model checker for UCTL has been realized, exploiting an on-the-fly algorithm. We then show how to use UCTL, and its model checker, in the design phase of an asynchronous extension of the communication protocol SOAP, called aSOAP. For this purpose, we describe aSOAP as a set of communicating UML state machines, for which a semantics over doubly labelled transition systems has been provided.
This work has been partially funded by the EU project Sensoria (IST-2005-016004) and by the Italian project tocai.it.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
ter Beek, M.H., Gnesi, S., Mazzanti, F., Moiso, C.: Formal Modelling and Verification of an Asynchronous Extension of SOAP. In: Bernstein, A., Gschwind, T., Zimmermann, W. (eds.) Proceedings of the 4th IEEE European Conference on Web Services (ECOWS 2006), Zurich, Switzerland, pp. 287–296. IEEE Computer Society, Los Alamitos, CA (2006)
Bhat, G., Cleaveland, R., Grumberg, O.: Efficient On-the-Fly Model Checking for CTL*. In: Proceedings of the 10th IEEE Symposium on Logics in Computer Science (LICS 1995), San Diego, CA, USA, pp. 388–397. IEEE Computer Society, Los Alamitos, CA (1995)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)
Chaki, S., Clarke, E.M., Grumberg, O., Ouaknine, J., Sharygina, N., Touili, T., Veith, H.: State/Event Software Verification for Branching-Time Specifications. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 53–69. Springer, Heidelberg (2005)
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects of Computing 17(4), 461–483 (2005)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM Transaction on Programming Languages and Systems 16(5), 1512–1542 (1994)
Cleaveland, R.: Tableau-Based Model Checking in the Propositional μ-Calculus. Acta Informatica 27(8), 725–747 (1989)
De Nicola, R., Vaandrager, F.W.: Actions versus State based Logics for Transition Systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
De Nicola, R., Vaandrager, F.W.: Three Logics for Branching Bisimulation. Journal of the ACM 42(2), 458–487 (1995)
Fernandez, J.-C., Jard, C., Jéron, T., Viho, C.: Using On-The-Fly Verification Techniques for the Generation of test Suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 348–359. Springer, Heidelberg (1996)
Gnesi, S., Mazzanti, F.: On the fly model checking of communicating UML State Machines. In: Dosch, W., Lee, R.Y., Wu, C. (eds.) SERA 2004. LNCS, vol. 3647, pp. 331–338. Springer, Heidelberg (2006)
Gnesi, S., Mazzanti, F.: A Model Checking Verification Environment for UML Statecharts. In: XLIII Annual Italian Conference AICA, Udine (2005)
Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM 32(1), 137–161 (1985)
Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Kindler, E., Vesper, T.: ESTL: A Temporal Logic for Events and States. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 365–384. Springer, Heidelberg (1998)
Mazzanti, F.: UMC User Guide v3.3. Technical Report 2006-TR-33, Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, CNR (2006)
Müller-Olm, M., Schmidt, D.A., Steffen, B.: Model-Checking—A Tutorial Introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)
OMG (Object Management Group), UML (Unified Modeling Language), http://www.uml.org/
Pnueli, A.: Linear and Branching Structures in the Semantics and Logics of Reactive Systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985)
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading, MA (1998)
Specification of aSOAP, http://fmt.isti.cnr.it/umc/examples/aSOAP.umc
Stirling, C., Walker, D.: Local Model Checking in the Modal μ-Calculus. In: Díaz, J., Orejas, F. (eds.) Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT 1989), Barcelona, Spain, vol. 354, pp. 369–383. Springer, Berlin (1989)
Wirsing, M., Clark, A., Gilmore, S., Hölzl, M., Knapp, A., Koch, N., Schroeder, A.: Semantic-Based Development of Service-Oriented Systems. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 24–45. Springer, Heidelberg (2006)
W3C (WWW Consortium), Latest SOAP versions, http://www.w3.org/TR/soap/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F. (2008). An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications . In: Leue, S., Merino, P. (eds) Formal Methods for Industrial Critical Systems. FMICS 2007. Lecture Notes in Computer Science, vol 4916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79707-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-79707-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79706-7
Online ISBN: 978-3-540-79707-4
eBook Packages: Computer ScienceComputer Science (R0)