Information Technology Reference
In-Depth Information
Methodologies for Specification of Real-Time
Systems Using Timed I/O Automata
AlexandreDavid
1
,KimG.Larsen
1
,AxelLegay
2
,
UlrikNyman
1
,andAndrzejWąsowski
3
1
ComputerScience,AalborgUniversity,Denmark
2
INRIA/IRISA,RennesCedex,France
3
ITUniversityofCopenhagen,Denmark
Abstract.
We present a real-time specification framework based on
Timed I/O Automata and a comprehensive tool support for it. The
framework supports various design methodologies including: top-down
refinement—fordecompositionofabstractspecificationstowardsincreas-
inglydetailed models;bottom-upabstraction—for synthesisofcomplex
systems from more concrete models; and step-wise modularisation of
requirements—tofactoroutbehavioursgivenbyexistingavailablecom-
ponents from a complex global requirements specification to be imple-
mented.Thesemethodologiesarerealizedbyconsecutiveapplicationsof
operators from the following set: refinement, consistency checking, log-
ical and structural composition and quotienting. Additionally, our tool
allows combining the component-oriented design process with verifica-
tionoftemporallogicpropertiesincreasingtheflexibilityoftheprocess.
1 Context and Motivation
Industriesdevelopingcomplexembeddedsystems,suchasaerospaceandauto-
motive,haveundergonedeeporganisationalchangeswithtremendousimpacton
developmentprocesses.Inthe past, theywereverticallyintegratedcompanies,
internallysupportingalldesignactivitiesfromspecificationtoimplementation.
Today they rely increasingly on external suppliers and on independent teams
toprovideessentialcomponentsofsystems.Itisnolongerpossibleforasingle
teamtocontroltheentiredesignprocessfromspecificationtoimplementation.
Complexsystemsemergefromassemblingmultiplecomponents.Thesecom-
ponentsaredesignedbyindependentlyworkingteams,whoadheretoacommon
agreement,a
contract
,onwhattheinterfaceofeachcomponentshouldbe.Such
aninterfacedefinesthebehavioursexpectedfromthecomponentaswellasthe
environmentin which it can be used. The main advantageis that it abstracts
fromthewaythecomponentcanbeimplemented.
Inpracticeinterfacesaredescribedusingtextualdocumentsormodellinglan-
guagessuchasUMLorWSDL.Unfortunately,suchspecificationsareambiguous
andthusaresubjecttointerpretation.Weinsteadrecommendrelyingonmath-
ematicallysoundformalismstoreduceambiguities.Inthiscontext,thevibrant
researchareaof
compositionalreasoning
[20]givesthefoundationsthatallowto
