Structured Interface Automata

Concurrency is a primitive notion in embedded systems. Threads enable concurrency at the software level by providing a mechanism of parallel execution. However, multithreaded programming can be an extremely tedious task. As the complexity of associated concerns escalates with the number of threads in the system, concurrent programming often becomes a bottleneck in the software engineering process. Therefore, the need for formal methods and tools facilitating the development of concurrent applications is becoming increasingly pressing.

This research project focuses on the formalization of a new interface theory [2] capturing the temporal aspects of concurrent components at the object-oriented programming level. Our formalism of structured interface automata heavily borrows from the interface automata of [1]. By imposing stronger constraints on the structure of the automata, we can appropriately steer the expressiveness of our language and effectively use it for design and validation, e.g. compatibility checking, deadlock and livelock detection, etc. Furthermore, we intend to employ this formalism for constructing a framework for systematic synchronization of concurrent objects, and supporting a polymorphic type system at the behavioral level, in accordance to [3].

[1] Luca de Alfaro and Thomas A. Henzinger. "Interface Automata". Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE), ACM Press, 2001, pp. 109-120.

[2] Luca de Alfaro and Thomas A. Henzinger. "Interface Theories for Component-Based Design". Proceedings of the First International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2211, Springer-Verlag, 2001, pp. 148-165.

[3] Edward A. Lee, and Yuhong Xiong. "Behavioral Types for Component-Based Designs". Technical Memorandum UCB/ERL, M02/29, University of California, Berkeley, CA 94720, USA, September 27, 2002.

Last updated 11/20/03