Component Reliability Extensions for Fractal Component Model

Project of

Institute of Computer Science
Academy of Sciences of the Czech Republic
&
France Telecom

Supported by France Telecom external research contract number 46127110.

Deliverable T0+18

Contacts at Institute of Computer Science:

Jiri Adamek
Tomas Bures
Pavel Jezek
Jan Kofron
Vladimir Mencl
Pavel Parizek
Frantisek Plasil

Contacts at France Telecom:

Nicolas Rivierre
Francois Horn
Thierry Coupaye

Purpose:

The purpose of this project is to extend the Fractal Component model and its Julia implementation with support for Behavior Protocols, originally published in IEEE Trans. Software Eng. 28(11), 1056-1076, 2002 and extended in the paper accepted for publication in Journal of Software Maintenance and Evolution: Research and Practice 17(5), Sep 2005.

Basic idea:

At ADL level, component specifications are equipped with their behavior description captured as Behavior Protocols. Advantageously, the behavior compliance of components can be checked at both and horizontal and vertical levels of component nesting. This checking can be done statically at design time, and dynamically at runtime. The static checking can detect several kinds of errors in component communication, including incomplete bindings. Static checking of protocol compliance can be done either via a standalone checker, or can be directly controlled by the Fractal ADL framework; in this case, the behavior protocols are specified directly in the ADL language. Runtime checking is achieved by monitoring the actual behavior on component interfaces and verifying whether it complies with the protocol; in Julia, the monitoring  is achieved via interceptors.

This deliverable (T0+18) consists of

  1. Extended protocol checker using source code/byte code analysis
  2. Prototype demonstration (testing the extended checker on the demo)
  3. Web documentation: architectural/design manual and user manual
To get acquainted with the new features provided by this deliverable, we recommend reading the Section 4.7 Cooperation of Java PathFinder with protocol checker, the Section 5.3 Cooperation of Java PathFinder with protocol checker and Section 6.5.1 Code analysis of primitive components: Getting Started of the User's manual.

Deliverable (T0+15) consists of

  1. Design of Java source code analysis and behavior protocol checking approach
To get acquainted with the new features provided by this deliverable, we recommend reading the Section 6.5.1 Code analysis of primitive components: Getting Started of the User's manual.

Deliverable (T0+12) consists of

  1. Testing the run-time checker on demo components
  2. Architecture/design manual and User manual
    (adding sections describing the run-time checker and the Julia integration).
To get acquainted with the new features provided by this deliverable, we recommend reading the Section 6.4.4. Case Study: Applying runtime-checker on the Airport internet lounge demo of the User's manual.

Deliverable (T0+9) consists of

  1. Runtime checker as a standalone component
  2. Runtime checker integrated into Julia
  3. Implementation of demo components
To get acquainted with the new features provided by this deliverable, we recommend reading the Section 6.4.1 Run-time checker: Getting Started of the User's manual.

Deliverable T0+6 consists of

  1. Static checker
    1. Integrated into Fractal
    2. Standalone
  2. Fractal extensions (protocols, runtime checking) + implementation
  3. Architecture/design manual and User manual
    (including small example to demonstrate how the extensions are used).
  4. Fractal extensions API documentation (Javadoc)
  5. Large application demo description. This contains description of an application (Airport Internet provision) consisting of over 20 components with behavior protocols.

Overview of new features developed within this project

  1. Protocol controller for Fractal components.
    To associate a component instance with a behavior protocol, a new controller (ProtocolController) for Fractal components is introduced.
  2. Extensions to Fractal ADL
    To accommodate behavior protocols in Fractal ADL descriptions, the Fractal ADL syntax is extended.
  3. Interceptors
    Support for runtime checking has been developed for Julia, utilizing the interceptor framework.
  4. Extensions to protocols
    Incomplete bindings, Collection interfaces, Multiple bindings, Atomic actions
  5. Checker improvements and enhancements
    New optimizations have been introduced into the checker, significantly improving performance. With these enhancements, the checker is able to handle large, real-life protocols. Enhancements also include visualization tools, important for understanding the reports of discovered errors.

Quick orientation: a recommendation

The recommended way to get acquainted with the basic idea and functionality of the deliverable is as follows:
  1. Behavior protocols basics
    Sect. 1.2.1. Behavior protocol basics
    Sect. 2.3. Frame and architecture protocols
  2. Static checker run to verify compliance
    Sect. 6.3.1. Getting Started
  3. Behavior protocols in Fractal ADL
    Sect. 6.1.1. Getting started
  4. Run-time checker
    Sect. 6.4.1 Getting Started
  5. Code analysis of primitive components
    Sect. 6.5.1 Getting Started
  6. Read systematically the manual
    Architecture/Design manual and User manual
  7. Study the demo to see a real-life example

Demo

Demo description: [PDF]
Demo overview diagram: [PDF]
Checkable protocol examples: [ZIP]
Output of "ant runtime-check": [TXT]
Output of "ant runtime-check-fail": [TXT]
Demo components implementation: included in the code distributions below.

Downloadable deliverables

Architecture/design manual: HTML PDF

Code (standalone checker, Fractal protocol extensions, runtime checker, demo components implementation): Binary Source code.
Javadoc API [HTML] [ZIP]

Demo Implementation Notes [HTML]

Publications related to the project

Refereed (journals/proceedings)
PDF Parizek, P., Plasil, F., Kofron, J.: Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker,
Accepted for publication in Proceedings of 30th IEEE/NASA Software Engineering Workshop (SEW-30), Columbia, MD, USA, April 25-27, 2006, IEEE Computer Society Press, Apr 2006
PDF Parizek, P., Plasil, F.: Specification and Generation of Environment for Model Checking of Software Components,
Accepted for publication in Proceedings of Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2006), Vienna, Austria, March 26, 2006, ENTCS, Mar 2006
PDF Mencl, V., Bures, T.: Microcomponent-Based Component Controllers: A Foundation for Component Aspects,
in Proceedings of 12th Asia-Pacific Software Engineering Conference (APSEC 2005), Dec 15-17, 2005, Taipei, Taiwan, pp. 729-738, ISBN 0-7695-2465-6, ISSN 1530-1362, IEEE Computer Society Press, Dec 2005
PDF Jezek, P., Kofron, J., Plasil, F.: Model Checking of Component Behavior Specification: A Real Life Experience,
Accepted for publication in Proceedings of International Workshop on Formal Aspects of Component Software (FACS'05), Macao, October 24-25, 2005, ENTCS, Oct 2005
Technical reports
PDF Kofron, J.: Enhancing Behavior Protocols with Atomic Actions,
Tech. Report No. 2005/8, Dep. of SW Engineering, Charles University, Prague, Nov 2005

ChangeLog


Contact

You may contact the project team by email at ft@d3s.mff.cuni.cz.