A new formalism for mathematical description and verification of component-based systems
Pages 334 - 353
Abstract
In this paper, we introduce a formal approach for composing software components into a distributed system. We describe the system as a hierarchical composition of some components, which can be distributed on a wide variety of hardware platforms and executed in parallel. We represent each component by a mathematical model and specify the abstract communication protocols of the components using Interface Automata (IAs). To model hierarchical systems, besides the basic components' model, we will present other components, called nodes. A node consists of a set of subnodes interacting under the supervision of a controller. Each subnode, in turn, is a node or discrete event component. By considering a subnode as a node we can make hierarchical nodes/components. The entire system, therefore, forms the root of the hierarchy. A controller, in turn, is a set of subcontrollers/interface automata that specifies interaction protocol of the components inside a node. We have also presented an example demonstrating the model by illustrating nodes, subnodes, controllers, and subcontrollers. To address the state space explosion problem in system verification, we utilize the controller as a contract for independent analysis of the components and their interactions. Therefore, a node will not be analyzed directly; instead, we will analyze the controller.
References
[1]
Arnold A (1994) Finite transition systems: semantics of communicating processes. Prentice Hall, New York.
[2]
Bernardo M, Ciancarini P, Donatiello L (2002) Families of software systems with process algebras. ACM TOSEM 11(4): 386-426.
[3]
Brim L, Cerna I, Varekova P, Zimmerova B (2006) Interaction automata as a verification-oriented component-based system specification. ACM SIGSOFT Softw Eng Notes 31(2): 1-8.
[4]
Bures T, Hnetynka P, Plasil F (2006) Balancing advanced features in a hierarchical component model. In: Proceedings of SERA, pp 40-48, Seattle, USA, IEEE CS, Aug 2006.
[5]
Cheung SC, Giannakopoulou D, Kramer J (1997) Verification of liveness properties using compositional reachability analysis. ACM SIGSOFT Softw Eng Notes Arch 22(6):227-243.
[6]
Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2): 244-263.
[7]
de Alfaro L, Henzinger T (2001) Interface automata. In: Proceedings of the joint 8th European software engineering conference and 9th ACM SIGSOFT symposium on the foundation of software engineering (ESEC/FSE-01), September 10-14 2001. 5 of software engineering notes, vol 26. ACM Press, New York, pp 109-120.
[8]
de Alfaro L, Henzinger T (2004) Interface-based design. In:Marktoberdorf summer school, pp 50-65. Kluwer, April 12-15 2004.
[9]
DePrince W, Hofmeister C (2003) Enforcing a lips usage policy for Corba components. In: EUROMICRO conf, new waves in system architecture, 2003, pp 53-60.
[10]
Jin Y, Lakos C, Esser R (2003) Component-based design and analysis: a case study. In: Software engineering and formal methods (SEFM). IEEE Computer Society Press, Los Alamitos, pp 126-135.
[11]
Jin Y, Lakos C, Esser R (2004) Modular consistency analysis of component-based designs. J Res Pract Inf Technol 36(3): 186-208.
[12]
Khammaci T, Smeda A, Oussalah M (2006) Mapping Cosa software architecture concepts into uml 2.0. icis-comsar 1: 109-114.
[13]
Leduc RJ (2007) Private communication, 2007. Department of Computing and Software, Faculty of Engineering, McMaster University, Canada.
[14]
Leduc RJ, Brandin BA, Lawford M, Wonham W (2005) Hierarchical interface-based supervisory control-part i: serial case. IEEE Trans Autom Control 50(9): 1322-1335.
[15]
Leduc RJ, Lawford M, Dai P (2006) Hierarchical interface-based supervisory control of flexible manufacturing system. IEEE Trans Control Syst Technol 14(4): 654-668.
[16]
Leduc RJ, Lawford M, Wonham W (2005) Hierarchical interface-based supervisory control-part ii: parallel case. IEEE Trans Autom Control 50(9): 1336-1348.
[17]
Magee J, Dulay N, Kramer J (1994) A constructive development environment for parallel and distributed programs. In: Proceedings of the international workshop on configurable distributed systems, Pittsburgh, March 1994, pp 4-14.
[18]
McMillan K (1992) Symbolic model checking: an approach to the state explosion problem. PhD thesis, Carnegie Mellon University, School of Computer Science.
[19]
Parnas DL (2000) Requirements documentation: why a formal basis is essential. In: Fourth IEEE international conference on requirements engineering (ICRE2000). Available online at: http://web.cps.msu.edu/sens/temp/ICRE2000/parnas.pdf.
[20]
Plasil F, Visnovsky S (2002) Behavior protocols for software components. IEEE Trans Softw Eng 28(11): 1056-1076.
[21]
Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium foundations of computer science (FOCS 1977), Providence, 1977, pp 46-57.
[22]
Schlingloff H (1997) Verification of finite-state systems with temporal logic model checking. South African Comput 19: 27-52.
[23]
Sistla AP (1994) Safety, liveness and fairness in temporal logic. J Formal Aspects Comput 6(5): 495- 511.
[24]
Smeda A, Khammaci T, Oussalah M (2004) Operational mechanisms for component-object based software architecture. In: Proceeding of information and communication technologies: from theory to applications, 19-23, April 2004, pp 591-592.
[25]
Szyperski C (2002) Component software: beyond object-oriented programming, 2nd edn. Addison-Wesley, Reading.
[26]
Xiong Y (2002) An extensible type system for component-based design. PhD thesis, Electronics Research Laboratory, University of California, Berkeley, May 2002.
Recommendations
Component-interaction automata as a verification-oriented component-based system specification
SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systemsIn the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-...
Component-interaction automata as a verification-oriented component-based system specification
In the paper, we present a new approach to component interaction specification and verification process which combines the advantages of both architecture description languages (ADLs) at the beginning of the process, and a general formal verification-...
Object-Oriented Component-Based Design using Behavioral Contracts: Application to Railway Systems
CBSE '15: Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software EngineeringIn this paper, we propose a formal approach for the design of object-oriented component-based systems using behavioral contracts. This formalism merges interface automata describing communication protocols of components with the semantics of their ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2009 Springer Science+Business Media, LLC.
Publisher
Kluwer Academic Publishers
United States
Publication History
Published: 01 September 2009
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 30 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in