Abstract
Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order in which the methods of a component are called, and output guarantees about the order in which the component calls external methods. The formalism supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Unlike traditional uses of automata, our formalism is based on an optimistic approach to composition, and on an alternating approach to design refinement. According to the optimistic approach, two components are compatible if there is some environment that can make them work together. According to the alternating approach, one interface refines another if it has weaker input assumptions, and stronger output guarantees. We show that these notions have game-theoretic foundations that lead to efficient algorithms for checking compatibility and refinement.
- 1 R. Allen and D. Garland. Formalizing architectural connection. In Proc. 16th IEEE Conf. Software Engineering, pages 71-80, 1994. Google ScholarDigital Library
- 2 R. Alur, T. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. In Concurrency Theory, Lecture Notes in Computer Science 1466, pages 163-178. Springer-Verlag, 1998. Google ScholarDigital Library
- 3 L. de Alfaro, T. Henzinger, and F. Mang. Detecting errors before reaching them. In Computer-Aided Verification, Lecture Notes in Computer Science 1855, pages 186-201. Springer-Verlag, 2000. Google Scholar
- 4 D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987. Google ScholarDigital Library
- 5 D. Jackson. Enforcing design constraints with object logic. In Static Analysis Sumposium, Lecture Notes in Computer Science 1824, pages 1-21. Springer-Verlag, 2000. Google Scholar
- 6 O. Kupferman and M. Vardi. Verification of fair transition systems. Chicago J. Theoretical Computer Science, 2, 1998. Google ScholarDigital Library
- 7 E. Lee and Y. Xiong. System-level Types for Component-based Design. Technical Memorandum UCB/ERL M00/8, Electronics Research Lab, University of California, Berkeley, 2000.Google Scholar
- 8 N. Leveson. System Safety and Computers. Addison-Wesley, 1995. Google Scholar
- 9 N. Lynch and M. Tuttle. Hierarcical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. Principles of Distributed Computing, pages 137-151, 1987. Google ScholarDigital Library
- 10 R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd International Joint Conference onArtificial Intelligence, pages 481-489. The British Computer Society, 1971.Google ScholarDigital Library
- 11 J. Reif. The complexity oftwo-player games of incomplete information. J. Computer and System Sciences, 29:274-301, 1984.Google ScholarCross Ref
- 12 J. Rumbaugh, G. Booch, and I. Jacobson. The UML Reference Guide. Addison-Wesley, 1999.Google Scholar
- 13 D. Yellin and R. Strom. Protocol specifications and component adapters. ACM Trans. Programming Languages and Systems, 19:292-333, 1997. Google ScholarDigital Library
Index Terms
- Interface automata
Recommendations
Interface automata
ESEC/FSE-9: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineeringConventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input ...
Formal verification of components assembly based on SysML and interface automata
We propose an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. So we propose to verify formally the assembly of components specified with the expressive ...
Revisiting modal interface automata
FormSERA '12: Proceedings of the First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile ApproachesModern software systems are typically built of components that communicate through their external interfaces. A component's behavior can be effectively described using finite state automata-based formalisms (e.g., statecharts [5]). The basic formalism, ...
Comments