Modal interfaces: unifying interface automata and modal specifications

ABSTRACT

This paper presents a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows to make assumptions on the environment and propose an optimistic view for composition : two components can be composed if there is an environment where they can work together. Modal specification is a language theoretic account of a fragment of the modal mu-calculus logic that is more complete but which does not allow to distinguish between the environment and the component. Partial unifications of these two frameworks have been explored recently. A first attempt by Larsen et al. considers modal interfaces, an extension of modal specifications that deals with compatibility issues in the composition operator. However, this composition operator is incorrect. A second attempt by Raclet et al. gives a different perspective, and emphasises on conjunction and residuation of modal specifications, including when interfaces have dissimilar alphabets, but disregards interface compatibility. The present paper contributes a thorougher unification of the two theories by correcting the modal interface composition operator presented in the paper by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing even further the comparison between interface automata, modal automata and modal interfaces.

REFERENCES

• 1: R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672--713, 2002.
• 2: R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi. Alternating refinement relations. In Proc. of the 9th International Conference on Concurrency Theory (CONCUR'98), volume 1466 of Lecture Notes in Computer Science, pages 163--178. Springer, 1998.
• 3: A. Arnold and M. Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theoretical Comput. Sci., 11, 1980.
• 4: N. Bertrand, S. Pinchinat, and J.-B. Raclet. Refinement and consistency of timed modal specifications. In Proc. of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), volume 5457 of Lecture Notes in Computer Science, pages 152--163, Tarragona, Spain, 2009. Springer.
• 5: S. Bliudze and J. Sifakis. A notion of glue expressiveness for component-based systems. In Proc. of the 19th International Conference on Concurrency Theory (CONCUR'08), volume 5201 of Lecture Notes in Computer Science, pages 508--522. Springer, 2008.
• 6: T. Brihaye, F. Laroussinie, N. Markey, and G. Oreiby. Timed concurrent game structures. In Proc. of the 18th International Conference on Concurrency Theory (CONCUR'07), volume 4703 of Lecture Notes in Computer Science, pages 445--459. Springer, 2007.
• 7: J. F. M. Burg. Linguistic instruments in requirements engineering. IOS Press, 1997.
• 8: A. Chakrabarti, L. de Alfaro, T. A. Henzinger, and F. Y. C. Mang. Synchronous and bidirectional component interfaces. In Proc. of the 14th International Conference on Computer Aided Verification (CAV'02), volume 2404 of Lecture Notes in Computer Science, pages 414--427, 2002.
• 9: Th. Chatain, A. David, and K. G. Larsen. Playing games with timed games. Research Report LSV-08-34, Laboratoire Specification et Verification, ENS Cachan, France, Dec. 2008. 15 pages.
• 10: W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1):45--80, 2001.
• 11: L. de Alfaro. Game models for open systems. In Verification: Theory and Practice, volume 2772 of Lecture Notes in Computer Science, pages 269--289. Springer, 2003.
• 12: L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable interfaces. In 5th International Workshop on Frontiers of Combining Systems (FroCos'05), volume 3717 of Lecture Notes in Computer Science, pages 81--105. Springer, 2005.
• 13: L. de Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga. The element of surprise in timed games. In Proc. of the 14th International Conference on Concurrency Theory (CONCUR'03), volume 2761 of Lecture Notes in Computer Science, pages 142--156. Springer, 2003.
• 14: L. de Alfaro and T. A. Henzinger. Interface automata. In Proc. of the 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE'01), pages 109--120. ACM Press, 2001.
• 15: L. de Alfaro, T. A. Henzinger, and M. Stoelinga. Timed interfaces. In Proc. of the 2nd Workshop on Embedded Software (EMSOFT'02), volume 2491 of Lecture Notes in Computer Science, pages 108--122. Springer, 2002.
• 16: L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov. Interface theories with component reuse. In L. de Alfaro and J. Palsberg, editors, Proc. of the 8th International Conference on Embedded Software (EMSOFT'08), pages 79--88. ACM Press, 2008.
• 17: J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Y. Xiong. Taming heterogeneity - the ptolemy approach. Proc. of the IEEE, 91(1):127--144, 2003.
• 18: G. Feuillade. Modal specifications are a syntactic fragment of the mu-calculus. Research Report RR-5612, INRIA, June 2005.
• 19: C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof. Stuck-free conformance. In Proc. of the 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 242--254. Springer, 2004.
• 20: T. A. Henzinger and J. Sifakis. The embedded systems design challenge. In Proc. of the 14th International Symposium on Formal Methods (FM'06), volume 4085 of Lecture Notes in Computer Science, pages 1--15. Springer, 2006.
• 21: ITU-TS. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva, September 1999.
• 22: K. G. Larsen. Modal specifications. In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 232--246. Springer, 1989.
• 23: K. G. Larsen, U. Nyman, and A. Wasowski. Modal I/O automata for interface and product line theories. In Programming Languages and Systems, 16th European Symposium on Programming (ESOP'07), volume 4421 of Lecture Notes in Computer Science, pages 64--79. Springer, 2007.
• 24: K. G. Larsen, U. Nyman, and A. Wasowski. On modal refinement and consistency. In Proc. of the 18th International Conference on Concurrency Theory (CONCUR'07), pages 105--119. Springer, 2007.
• 25: G. Luttgen and W. Vogler. Conjunction on processes: Full abstraction via ready-tree semantics. Theoretical Computer Science, 373:19--40, 2007.
• 26: N. Lynch and M. R. Tuttle. An introduction to Input/Output automata. CWI-quarterly, 2(3), 1989.
• 27: U. Nyman. Modal Transition Systems as the Basis for Interface Theories and Product Lines. PhD thesis, Aalborg University, Department of Computer Science, September 2008.
• 28: J.-B. Raclet. Quotient de specifications pour la reutilisation de composants. PhD thesis, Universite de Rennes I, december 2007. (In French).
• 29: J.-B. Raclet. Residual for component specifications. In Proc. of the 4th International Workshop on Formal Aspects of Component Software (FACS'07), 2007.
• 30: J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, and R. Passerone. Why are modalities good for interface theories? In Proc. of the 9th International Conference on Application of Concurrency to System Design (ACSD'09). IEEE Computer Society Press, 2009.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.12 Interoperability
            Subjects: Interface definition languages

General Terms:
Design, Theory

Keywords:
compatibility, interface automata, modal specifications