Cadena: an integrated development, analysis, and verification environment for component-based systems
- 1 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02705257,p. 160-172
- https://doi.org/10.1109/icse.2003.1201197
Abstract
The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution. To form an effective basis for development of such systems, we believe that support for reasoning about correctness properties of component-based designs is essential. In this paper, we present Cadena - an integrated environment for building and modeling CCM systems. Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition System semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM IDL, component assembly information, and Cadena specifications, and producing CORBA stubs and skeletons implemented in Java. We are applying Cadena to avionics applications built using Boeing's Bold Stroke framework.Keywords
This publication has 16 references indexed in Scilit:
- vUML: a tool for verifying UML modelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Reducing avionics software cost through component based product line developmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Events and constraints: a graphical editor for capturing logic requirements of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Model checking implicit-invocation systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- NUSMV: a new symbolic model checkerInternational Journal on Software Tools for Technology Transfer, 2000
- Model checking JAVA programs using JAVA PathFinderInternational Journal on Software Tools for Technology Transfer, 2000
- Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checkerFormal Aspects of Computing, 1999
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- A Practitioner’s Handbook for Real-Time AnalysisPublished by Springer Nature ,1993
- The use of program dependence graphs in software engineeringPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1992