Abstract
Distributed systems for open environments, like the Internet, are becoming more frequent and important. However, it is difficult to assure that such systems have the required functional properties. In this paper we use a visual formal specification language, called Object-Based Graph Grammars (OBGG), to specify asynchronous distributed systems. After discussing the main concepts of OBGG, we propose an approach for the verification of OBGG specifications using model checking. This approach consists on the translation of OBGG specifications into PROMELA (PROcess/PROtocol MEta LAnguage), which is the input language of the SPIN model checker. The approach we use for verification allows one to write properties based on the OBGG specification instead of on the generated PROMELA model.
This work is partially supported by HP Brasil – PUCRS agreement CASCO (24o TA.), ForMOS (FAPERGS/CNPq), PLATUS (CNPq), IQ-Mobile II (CNPq/CNR) and DACHIA (FAPERGS/IB-BMBF) Research Projects.
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
Chechik, M., Păun, D.O.: Events in property patterns. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 154–167. Springer, Heidelberg (1999)
Cho, S.M., et al.: Applying model checking to concurrent object-oriented software. In: 4th International Symposium on Autonomous Decentralized Systems, Japan, pp. 380–383. IEEE Computer Society Press, Los Alamitos (1999)
Copstein, B., Mora, M.C., Ribeiro, L.: An environment for formal modeling and simulation of control systems. In: 33rd Annual Simulation Symposium, USA, pp. 74–82. IEEE Computer Society, Los Alamitos (2000)
Dotti, F.L., Duarte, L.M., Copstein, B., Ribeiro, L.: Simulation of mobile applications. In: Communication Networks and Distributed Systems Modeling and Simulation Conference, The Society for Modeling and Simulation International, USA, pp. 261–267 (2002)
Dotti, F.L., Duarte, L.M., Silva, F.A., Andrade, A.S.: A framework for supporting the development of correct mobile applications based on graph grammars. In: 6th World Conference on Integrated Design & Process Technology, Society for Design and Process Science, USA, pp. 1–9 (2002)
Dotti, F.L., Ribeiro, L.: Specification of mobile code systems using graph grammars. In: Programming Languages and their Definition. IFIP Conference Proceedings, USA, vol. 177, pp. 45–63. Kluwer, Dordrecht (1984)
Dotti, F.L., Santos, O.M., Rödel, E.T.: On the use of formal specifications to analyze fault behaviors of distributed systems. In: 1st Latin-American Symposium on Dependable Computing, Germany. LNCS. Springer, Heidelberg (2003) (accepted)
Ehrig, H.: Introduction to the algebraic theory of graph grammars. In: 1st International Workshop on Graph Grammars and Their Application to Computer Science and Biology, Germany. LNCS, vol. 73, pp. 1–69. Springer, Heidelberg (1979)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Leue, S., Holzmann, G.: v-Promela: a visual, object oriented language for SPIN. In: 2nd International Symposium on Object-Oriented Real-Time Distributed Computing, France, pp. 14–23. IEEE Computer Society Press, Los Alamitos (1999)
Lilius, J., Paltor, I.P.: vUML: a tool for verifying UML models. In: 14th International Conference on Automated Software Engineering, USA, pp. 255–258. IEEE Computer Society Press, Los Alamitos (1999)
Loreto, A.B., Ribeiro, L., Toscani, L.V.: Decidability and tractability of a problem in object-based graph grammars. In: Selman, A.L. (ed.) Structure in Complexity Theory. LNCS, vol. 223, pp. 396–408. Kluwer, Dordrecht (2002)
Ribeiro, L., Copstein, B.: Compositional construction of simulation models using graph grammars. In: Münch, M., Nagl, M. (eds.) AGTIVE 1999. LNCS, vol. 1779, pp. 87–95. Springer, Heidelberg (2000)
Rozenberg, G. (ed.): Handbook of graph grammars and computing by graph transformation. Foundations, vol. 1. World Scientific, Singapore (1997)
Weise, C.: An incremental formal semantics for PROMELA. In: 3rd SPIN Workshop, The Netherlands (1997)
Winter, K., Duke, R.: Model checking object-Z using ASM. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 165–184. Springer, Heidelberg (2002)
Promela language reference (2003), http://spinroot.com/spin/Man/promela.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Dotti, F.L., Foss, L., Ribeiro, L., dos Santos, O.M. (2003). Verification of Distributed Object-Based Systems. In: Najm, E., Nestmann, U., Stevens, P. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2003. Lecture Notes in Computer Science, vol 2884. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39958-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-39958-2_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20491-6
Online ISBN: 978-3-540-39958-2
eBook Packages: Springer Book Archive