Information Technology Reference
In-Depth Information
reasonaboutpropertiesofthe globalsystembasedon propertiesofindividual
components.The essentialadvantageofcompositionalreasoningisits support
forsafereuseofcomponents,wellknownfromotherengineeringdisciplines.
Building specification theories is a subject of intensive studies[11,14]. One
particularly successful direction are interface automata[14,15,23,31]. In this
framework,aninterfaceisrepresentedbyaninput/outputautomaton[29],where
transitions are typed as
input
and
output
. The semantics is given by a two-
playergame:the
input
playerrepresentstheenvironment,andthe
output
player
represents the component itself. Contrary to the input/output model of[29],
this semanticoffersanoptimistictreatmentofcomposition:twointerfacescan
becomposedifthereexistsanenvironmentinwhichtheycansafelyinteract.
Theexistinginterfacetheoriesfocusprimarilyoncomposition(andsometimes
onrefinement).Therehardlyexistsupportingtoolsthatcouldbeusedbyengi-
neers.Overtheyearsofinteractionwithindustrialpartners,wehavecollected
thefollowingrequirementsforinterfacestheories.Noticethattheysignificantly
exceedtheusualscopeofstudyingcompositionandrefinement.
1. Itshouldbedecidablewhetheraninterfaceadmitsanimplementation.
1
2. Theremustbeamechanismtosafelyreplaceacomponentbyanotherone.
Technicallythiscorrespondstotherequirementsofprecongruenceandcom-
pletenessfor
Refinement
.Refinement(written
),whichisapreorderonthe
setofinterfaces,shouldsatisfythefollowingproperty:
Everyimplementationsatisfyingarefinementofaninterfaceshould
alsosatisfythisinterface.
3. To control design complexity, one should be able to decide whether there
existsaninterfacethatrefinestwodifferentinterfaces(a
sharedrefinement
).
4. Differentaspectsofsystemsareoftenspecifiedbydifferentteams.Theissue
ofdealingwithmultipleaspectsormultiple viewpointsisthusessential.It
shouldbepossibletorepresentseveralinterfaces(viewpoints)forthesame
component,andtocombinetheninaconjunctivefashion.Conjunction(writ-
ten
≤
∧
)shouldsatisfythefollowingproperty:
Given two viewpoints represented by two interfaces, any implemen-
tationthatsatisfiestheconjunctionmustsatisfythetwoviewpoints.
5. Theframeworkshouldprovideacombinationoperationreflectingthestan-
dardinteractionbetweensystems.Itshouldrespecttherefinementto sup-
portindependentdevelopment:
Giventwoimplementationsoftwointerfaces,thecompositionofthe
implementations satisfiesthecomposition oftheir interfaces.
6. Itshouldbepossibletofactorinexistingcomponentsintogeneralrequire-
ments,inordertofacilitatereuseofaccumulatedassets.Ininterfacetheories
thisisrealizedusingaquotientoperator.
7. Conjunctionandcompositionmustbeassociativeandcommutative,sothat
the emergent behaviour of the system depends only on the specifications,
notontheorderinwhichtheyhavebeencombined.
1
In our theory, an implementation shall not be viewed as a program in a concrete
programminglanguagebutratherasanabstractmathematicalobjectthatrepresents
asetofprogramssharingcommonproperties.
