research
& development
Towards a Versatile
Contract Model to Organize Behavioral Specifications
Philippe Collet1,
Alain Ozanne2 and Nicolas Rivierre2
1. University of Nice, I3S Laboratory, France
2. France Telecom R&D, France
research
& development
France
Telecom Group
- Dependability : assembly validity (requirements satisfaction),
- Robustness : diagnosis, failure repair,
Context: Assembled
Applications
service
component
- Properties complexity :
kinds: QoS (SLA..), behavior (service interaction00, 00[Beugnard] formalisms: CQML, Quo, assertions, Behavior Protocol00/font>- Dynamic evolutions
Sound Composition
research
& development
France
Telecom Group
Motivations
and Requirements
A tool that deals with various properties and verifications means
A tool compatible with the dynamic evolutions of architectures
A tool conceptually as secure and explicit as real life contracts
research
& development
France
Telecom Group
Goal: a Contracting
Framework
P1 : Makes explicit the conformity of individual components with their specification Conformity
P2 : Makes explicit, for a configuration of components, the compatibility of their specifications Compatibility
P3 : Makes explicit the responsibilities of the components against their specifications Responsibilities
P4 : Supports various specification formalisms and verification techniques Formalisms
research
& development
France
Telecom Group
Related Work
Conformity
Compatibility
Responsibility
Various formalisms
Existing frameworks
Goal
J2EE
research
& development
France
Telecom Group
System
Interface Contract
assertion scope = interface
ConFract:
- Assertions associated with a component
- Components00conformity to assertions
- Associated responsibility
External Composition Contract
assertion scope = component00
outside
Internal Composition Contract
assertion scope = composite00 inside
research
& development
France
Telecom Group
Contract Model
Participant
Clause
Participant
Participant
Clause
Agreement
Assumption
Guarantee
Guarantee
Assumption
Clause
Assumption
Guarantee
Clauses satisfaction + Agreement satisfaction => Sound Composition
research
& development
France
Telecom Group
Contract and
Formalisms
Constraint description :
Contract
{
Participants : <component_name>* ;
Clauses :
{
clause : <name>
responsible : <component_name> ;
assumption : < constraint >
guarantee : < constraint >
} *
Agreement : { agreement : < constraint >*}
}
On <component_name>
Observe : ( val : <some values> at : <some events>; ) +
Verify : < predicate
>
P1
P3
P2
P4
Component specification
Contractual formalism
research
& development
France
Telecom Group
Behavior Protocols
Regular-like expressions <speedCtrl> : (?ppt.enable; !csp.setThrottle*; ?ppt.disable)*
Tools are provided to check Implementation conformity Protocols compatibility (horizontal and vertical)
research
& development
France
Telecom Group
Application
of Behavior Protocols
<speedCtrl>
(?ppt.enable; !csp.setThrottle*; ?ppt.disable)*
<sensorCtrl>
?sns.engineOn; (?sns.on; !ppt.enable; (?sns.accelerate +
?sns.brake + ?sns.off)*; !ppt.disable)*
+ ?sns.engineOff
<CruiseCtrl>
?sns.engineOn; (?sns.on; !csp.setThrottle*; (?sns.accelerate
+ ?sns.brake + ?sns.off)*)* + ?sns.engineOff
research
& development
France
Telecom Group
Resulting Contract
(1/2)
Contract :
Participants : <SensorCtrl>, <CruiseCtrl>, <SpeedCtrl> ;
...
Clause :
responsible : <SpeedCtrl>
assumption :
On <SpeedCtrl>
Observe : val : at entry ppt.*;
Verify : runtimeCheck(speedCtrlFP);
guarantee :
On <SpeedCtrl>
Observe : val : at entry csp.*;
Verify : runtimeCheck(speedCtrlFP);
...
<SpeedCtrl>
speedCtrlFP = (?ppt.enable;
!csp.setThrottle*; ?ppt.disable)*
ppt
csp
research
& development
France
Telecom Group
Resulting Contract
(2/2)
Contract :
Participants : <SensorCtrl>, <CruiseCtrl>, <SpeedCtrl> ;
...
Agreement :
On <CruiseCtrl>
Observe : val : at : entry <CruiseCtrl>.start
Verify : verticalCheck (cruiseCtrlFP, parallelCheck (sensorCtrlFP,
speedCtrlFP))
<SensorCtrl>
<SpeedCtrl>
<CruiseCtrl>
verticalCheck
parallelCheck
research
& development
France
Telecom Group
Contract for
Assertion-based Formalism
float
getResponseTime(float throttle)
<SpeedCtrl>
<CruiseCtrl>
csp
Clause : <CruiseCtrl>
Clause : <SpeedCtrl>
Clause : <SpeedCtrl>
A =
G =
G =
A =
pre : throttle > 10
post : return > 0
Client side
<SpeedCtrl>
pre : throttle > 0
post : return > 10
Server side
<CruiseCtrl>
Agreement :
return > 10 => return > 0
throttle > 10 => throttle > 0
research
& development
France
Telecom Group
Integration
and Use
Framework
R1. Formalisms
integrator
R2.Domain specifier
R3. User of the results of the contract
evaluation
Checking
Building
Integration to the framework core
Mechanism
Contracts
Specifications, System
R2
-
Adapter (Plugin) :
Formalism translator
Provides
A contract builder and checker
R1
Garantuees / diagnosis
R3
Obtains
Role
Fractal System
Pre/post conditions
Example of use with an assertion translator
:
Guarantee
Checking
Observations
Contractual Spec.
Contract
Building
research
& development
France
Telecom Group
Conclusion
Supports the expected properties provided that: Specifications can be translated in assumption-guarantee constraints Specifications have tools for checking conformity and compatibility
Simple and pragmatic principles for software architects
Future works : Vertical composition of contracts between consecutive levels of nesting (when the formalism supports it), Application to other architectural platforms (components, services00
research
& development
France
Telecom Group
Questions
download Towards a Versatile Contract Model to Organize Behavioral ...
