A Modal Interface Theory for Component-based Design

• Autorzy: Raclet J. B. , Benveniste A. , Legay A. , Badouel E. , Caillaud B. , Passerone R.
• Języki publikacji: EN

Abstrakty

EN

This paper presents the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-basedmodel, which allows the designer to express assumptions on the environment and which uses an optimistic view of composition: two components can be composed if there is an environment where they can work together. Modal specifications are a language theoretic account of a fragment of the modal mu-calculus logic with a rich composition algebra which meets certain methodological requirements but which does not allow the environment and the component to be distinguished. The present paper contributes a more thorough unification of the two theories by correcting a first attempt in this direction by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing the comparison between interface automata, modal automata and modal interfaces even further. The work reported here is based on earlier work presented in [41] and [42].

Słowa kluczowe

EN

component-based system; compositional reasoning; interface theory; interface automata; modal specifications

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 108, nr 1/2
• Strony: 119--149
• Opis fizyczny: Bibliogr. 43 poz.

Twórcy

autor

Raclet J. B.

autor

Benveniste A.

autor

Legay A.

autor

Badouel E.

autor

Caillaud B.

autor

Passerone R.

• INRIA Grenoble - Rh�ones-Alpes, France,

Bibliografia

• [1] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the 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 Lecture Notes in Computer Science 1466, pages 163-178. Springer, 1998.
• [3] A. Antonik, M. Huth, K. G. Larsen, U. Nyman, and A. Wasowski. Complexity of decision problems for mixed and modal specifications. In Proc. of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), volume Lecture Notes in Computer Science 4962, pages 112-126. Springer, 2008.
• [4] A. Arnold and M. Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theoretical Computer Science, 11, 1980.
• [5] E. Badouel, A. Benveniste, B. Caillaud, T. A. Henzinger, A. Legay, and R. Passerone. Contract theories for embedded systems : A white paper. Research report, IRISA/INRIA Rennes, 2009.
• [6] N. Benes, J. Kret´ınsk´y, K. G. Larsen, and J. Srba. On determinism in modal transition systems. Theoretical Computer Science, 410(41):4026-4043, 2009.
• [7] A. Benveniste, B. Caillaud, and R. Passerone. A generic model of contracts for embedded systems. Research report 6214, IRISA/INRIA Rennes, 2007.
• [8] N. Bertrand, A. Legay, S. Pinchinat, and J.-B. Raclet. A compositional approach on modal specifications for timed systems. In Proc. of the 11th International Conference on Formal Engineering Methods (ICFEM'09), volume Lecture Notes in Computer Science 5885, pages 679-697. Springer, 2009.
• [9] 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 Lecture Notes in Computer Science 5457, pages 152-163. Springer, 2009.
• [10] P. Bhaduri. Synthesis of interface automata. In Proc. of the 3rd Automated Technology for Verification and Analysis Conference (ATVA'05), volume Lecture Notes in Computer Science 3707, pages 338-353. Springer, 2005.
• [11] 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 Lecture Notes in Computer Science 5201, pages 508-522. Springer, 2008.
• [12] 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 Lecture Notes in Computer Science 4703, pages 445-459. Springer, 2007.
• [13] 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 Lecture Notes in Computer Science 2404, pages 414-427. Springer, 2002.
• [14] T. Chatain, A. David, and K. G. Larsen. Playing games with timed games. In Proc. of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS'09), 2009.
• [15] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branchingtime temporal logic. In Logic of Programs, volume Lecture Notes in Computer Science 131, pages 52-71. Springer, 1981.
• [16] D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253-291, 1997.
• [17] L. de Alfaro. Game models for open systems. In Verification: Theory and Practice, volume Lecture Notes in Computer Science 2772, pages 269-289. Springer, 2003.
• [18] L. de Alfaro, L. Dias da Silva, M. Faella, A. Legay, P. Roy, and M. Sorea. Sociable interfaces. In Proc. Of the 5th International Workshop on Frontiers of Combining Systems (FroCos'05), volume Lecture Notes in Computer Science 3717, pages 81-105. Springer, 2005.
• [19] 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 Lecture Notes in Computer Science 2761, pages 142-156. Springer, 2003.
• [20] 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.
• [21] L. de Alfaro, T. A. Henzinger, andM. Stoelinga. Timed interfaces. In Proc. of the 2ndWorkshop on Embedded Software (EMSOFT'02), volume Lecture Notes in Computer Science 2491, pages 108-122. Springer, 2002.
• [22] L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov. Interface theories with component reuse. In Proc. of the 8th International Conference on Embedded Software (EMSOFT'08), pages 79-88. ACM Press, 2008.
• [23] 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.
• [24] G. Feuillade and S. Pinchinat. Modal specifications for the control theory of discrete-event systems. Discrete Event Dynamic Systems, 17(2):181-205, 2007.
• [25] 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 Lecture Notes in Computer Science 3114, pages 242-254. Springer, 2004.
• [26] P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based model checking using modal transition systems. In Proc. of the 12th International Conference on Concurrency Theory (CONCUR'01), volume Lecture Notes in Computer Science 2154, pages 426-440. Springer, 2001.
• [27] G. Goessler and J.-B. Raclet. Modal contracts for component-based design. In Proc. of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09), pages 295-303. IEEE Computer Society Press, 2009.
• [28] O. Grumberg, M. Lange, M. Leucker, and S. Shoham. Don't know in the μ-calculus. In Proc. of the 6th International Conference on Verification,Model Checking, and Abstract Interpretation (VMCAI'05), volume Lecture Notes in Computer Science 3385, pages 233-249. Springer, 2005.
• [29] T. A. Henzinger and J. Sifakis. The embedded systems design challenge. In Proc. of the 14th International Symposium on Formal Methods (FM'06), volume Lecture Notes in Computer Science 4085, pages 1-15. Springer, 2006.
• [30] K. G. Larsen. Modal specifications. In Automatic Verification Methods for Finite State Systems, volume Lecture Notes in Computer Science 407, pages 232-246. Springer, 1989.
• [31] K. G. Larsen, U. Nyman, and A. Wasowski. Modal I/O automata for interface and product line theories. In Proc. of the 16th European Symposium on Programming Languages and Systems (ESOP'07), volume Lecture Notes in Computer Science 4421, pages 64-79. Springer, 2007.
• [32] 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), volume Lecture Notes in Computer Science 4703, pages 105-119. Springer, 2007.
• [33] G. Lüttgen and W. Vogler. Conjunction on processes: Full abstraction via ready-tree semantics. Theoretical Computer Science, 373:19-40, 2007.
• [34] N. Lynch and M. R. Tuttle. An introduction to Input/Output automata. CWI-quarterly, 2(3), 1989.
• [35] R. Milner. A complete axiomatisation for observational congruence of finite-state behaviors. Information and Computation, 81(2):227-247, 1989.
• [36] U. Nyman. Modal Transition Systems as the Basis for Interface Theories and Product Lines. PhD thesis, Aalborg University, Department of Computer Science, 2008.
• [37] A. Pnueli. The temporal logic of programs. In Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS'77), pages 46-57, 1977.
• [38] S. Quinton and S. Graf. Contract-based verification of hierarchical systems of components. In Proc. of the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM'08), pages 377-381. IEEE Computer Society, 2008.
• [39] J.-B. Raclet. Quotient de spécifications pour la réutilisation de composants. PhD thesis, Université de Rennes I, 2007. (In French).
• [40] J.-B. Raclet. Residual for component specifications. In Proc. of the 4th International Workshop on Formal Aspects of Component Software (FACS'07), volume Electronic Notes Theoretical Computer Science 215, pages 93-110, 2008.
• [41] J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay, and R. Passerone. Modal interfaces: Unifying interface automata and modal specifications. In Proc. of the 9th International Conference on Embedded Software (EMSOFT'09), pages 87-96. ACM Press, 2009.
• [42] 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), pages 199-127. IEEE Computer Society Press, 2009.
• [43] J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, and R. Passerone. Why aremodalities good for Interface Theories? Research Report RR-6899, INRIA, 2009.