A Modal Specification Theory for Components with Data

  • Sebastian S. Bauer
  • Kim Guldstrand Larsen
  • Axel Legay
  • Ulrik Nyman
  • Andrzej Wąsowski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7253)


Modal specification is a well-known formalism used as an abstraction theory for transition systems. Modal specifications are transition systems equipped with two types of transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows to develop a unique approach for both logical and structural compositions, and eases the step-wise refinement process for building implementations.

We propose Modal Specifications with Data (MSD), the first modal specification theory with explicit representation of data. Our new theory includes all the essential ingredients of a specification theory. As MSD are by nature potentially infinite-state systems, we propose symbolic representations based on effective predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.


Model Check Transition System Parallel Composition Structural Composition Require Behavior 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  2. 2.
    Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer (1980)Google Scholar
  3. 3.
    Nyman, U.: Modal Transition Systems as the Basis for Interface Theories and Product Lines. PhD thesis, Department of Computer Science, Aalborg University (October 2008)Google Scholar
  4. 4.
    Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: Modal interfaces: unifying interface automata and modal specifications. In: Chakraborty, S., Halbwachs, N. (eds.) EMSOFT. ACM (2009)Google Scholar
  5. 5.
    Abdulla, P.A., Bouajjani, A., d’Orso, J.: Monotonic and downward closed games. J. Log. Comput. 18(1), 153–169 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-Based Model Checking Using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109–127 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable Interfaces. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 81–105. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108–117. IEEE Computer Society (1990)Google Scholar
  10. 10.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society (1988)Google Scholar
  11. 11.
    Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wąsowski, A.: Complexity of Decision Problems for Mixed and Modal Specifications. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 112–126. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Larsen, K.G., Nyman, U., Wąsowski, A.: On Modal Refinement and Consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105–119. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Benes, N., Kretínský, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Theor. Comput. Sci. 410(41), 4026–4043 (2009)zbMATHCrossRefGoogle Scholar
  14. 14.
    de Alfaro, L., Henzinger, T.A.: Interface Theories for Component-Based Design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Bauer, S.S., Hennicker, R., Wirsing, M.: Interface theories for concurrency and data. Theor. Comput. Sci. 412(28), 3101–3121 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O Automata for Interface and Product Line Theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Raclet, J.-B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)CrossRefGoogle Scholar
  18. 18.
    Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  19. 19.
    van de Pol, J., Valero Espada, M.: Modal Abstractions in μCRL. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 409–425. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26, 109–120 (2001)CrossRefGoogle Scholar
  21. 21.
    Lynch, N., Tuttle, M.R.: An introduction to Input/Output automata. CWI-quarterly 2(3) (1989)Google Scholar
  22. 22.
    Fernandes, F., Royer, J.-C.: The STSLib project: Towards a formal component model based on STS. Electr. Notes Theor. Comput. Sci. 215, 131–149 (2008)CrossRefGoogle Scholar
  23. 23.
    Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural models for distributed fractal components. Annales des Télécommunications 64(1-2), 25–43 (2009)CrossRefGoogle Scholar
  24. 24.
    Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On Weak Modal Compatibility, Refinement, and the MIO Workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  25. 25.
    Bauer, S.S., Mayer, P., Legay, A.: MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 418–421. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Sebastian S. Bauer
    • 1
    • 2
  • Kim Guldstrand Larsen
    • 2
  • Axel Legay
    • 3
  • Ulrik Nyman
    • 2
  • Andrzej Wąsowski
    • 4
  1. 1.Institut für InformatikLudwig-Maximilians-Universität MünchenGermany
  2. 2.Department of Computer ScienceAalborg UniversityDenmark
  3. 3.INRIA/IRISARennesFrance
  4. 4.IT University of CopenhagenDenmark

Personalised recommendations