Symbolic semantics and verification of stochastic process algebras [Elektronische Ressource] = Symbolische Semantik und Verifikation stochastischer Prozessalgebren / vorgelegt von Georg Wolfgang Matthias Kuntz

Sujets

• Informatik

Informations

• Publié par: friedrich-alexander-universitat_erlangen-nurnberg
• Publié le: 01 janvier 2006
• Nombre de lectures: 4
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Symbolic Semantics and Verification of
Stochastic Process Algebras
Symbolische Semantik und Verifikation
stochastischer Prozessalgebren
DerTechnischenFakultätder
UniversitätErlangen-Nürnberg
zurErlangungdesGrades
DOKTOR-INGENIEUR
vorgelegtvon
GeorgWolfgangMatthiasKuntz
Erlangen-2006AlsDissertationgenehmigtvon
derTechnischenFakultätder
UniversitätErlangen-Nürnberg
TagderEinreichung:14.10.2005
TagderPromotion:02.02.2006
Dekan:Prof.Dr.-Ing.AlfredLeipertz
Berichterstatter:Prof.Dr.-Ing.MarkusSiegle
Prof.Dr.-Ing.ReinhardGermanSummary
Intherealmofperformanceandreliabilityanalysis,high-levelspecificationlanguageslike
stochastic processalgebras (SPA)or generalisedstochastic Petri nets (GSPN)have turned
out to be extremely useful. During the analysis of systems, being specified with either of
thetwomethods,twomainproblemscanbeidentified:
1. Statespaceexplosion: This problemoccurs on generation andstorage ofthe semantic
models of complex systems on which analysis is carried out. This semantic model is
normallysomekindofacontinuoustimeMarkovchain(CTMC)orstochasticlabelled
transitionsystem(SLTS).
2. Thespecificationandautomaticverificationofcomplexsystemrequirements
The state space explosion problem arises mainly in the context of the analysis of concur-
rentsystems.Thisisthetypeofsystems,forwhichwewanttodeviseanalysismethodsin
thisthesis.IfthesystemisspecifiedusingSPAs,itiscomposedofmanyparallelprocesses.
TheoverallstatespaceofsuchamodelisthentheCartesianproductofthestatespacesof
therespectivesubprocesses.Thus,thememoryrequirementsforstoringtheSLTSsofcom-
plexsystemsareoftenprohibitive.Tocombatthisproblemseveralstepsmustbetaken.At
first,datastructuresthatallowthecompactstorageofevenhugestatespacesmustbeap-
plied. Multi-terminal binary decision diagrams (MTBDD)turned out to be advantageous
in the storage of large SLTSs. Secondly, upon generation of the SLTSs, the fact that SPA
specifications are normally composed of many smaller subprocesses has to be taken into
account.ThetraditionalsemanticsofSPAssupportsthisonlyinaverylimitedway.These
semantics only support a monolithic way of state space generation which turned out to
have exponential memory requirements. To avoid this, we devise a new semantics that
utilises the structureof agivenSPA specification upon generation ofits underlying SLTS.
Foreverysubprocessofagiven specificationwederivetheMTBDDbasedrepresentation
ofitscorrespondingSLTS.Accordingtothesyntacticstructureofthespecificationathand,
theoverallMTBDDrepresentationcanbederivedfromthesubprocesses’MTBDDs.Itcan
be shown that the memory requirement for an semantic approach that utilises the com-
positional nature of process algebras is only linear, opposed to an exponential memory
requirementinthecaseoftraditionalSPAsemantics.
In the second part of this thesis we address the problem of automatically verifying
performanceandreliabilityrequirements.Here,threesubproblemscanbeidentified:
1. Complexityofrequirements
2. AbstractionVIII Summary
3. Efficientnumericalanalysis
Usually,intraditionalperformanceandreliabilityanalysisonlyquitesimplerequirements
areexpressible.Forexample:
• Meannumberofjobsinasystem,
• theprobability,thatasystemisoperationaloveraperiodoftime,
• themeantimetofailure,meantimetorepair.
Because of this in the recent years, efforts have been made to transfer the means that are
providedbyfunctionalmodelcheckingtothestochasticworld(modelcheckingofstochas-
ticsystems).Wewillfurtherrefinethisapproachinthisthesis,whichcanbebestexplained
incontextwiththeproblemofabstraction.Theproblemofabstractionstemsfromthefact
thatbothintraditionalperformanceandreliabilityanalysisandmodelcheckingofstochas-
tic systems, the requirementshaveto beformulatedwith thesemantic model in mind. To
defineusefulrequirementsdetailedknowledgeaboutthestructureoftheunderlyingstate
space is required.This contradicts both the usage of high-level specification languages in
generalandtheusageofSPAsinparticular.Ingeneral,theapplicationofhigh-levelmeth-
ods shall free the user from the need to have knowledge about low-level details, such as
thesemanticmodel.InparticulartheusageofSPAsasspecificationlanguagemakesitpos-
sibletothinkofthesystembehaviourasasequenceofactions,statesdonotplayarolein
thiscontext.Thus,referringtostateshere,isnotonlyaviolationoftheprincipleofabstrac-
tionbutalsomeansadisturbingshiftofparadigmsfromanaction-toastateorientedview
ofthemodelledsystem.Toavoidtheseproblems,i.e.violationoftheabstractionprinciple
and the shift of paradigms, we develop a new stochastic logic in this thesis. This logic is
a stochastic extension of the logic PDL (propositional dynamic logic), called SPDL. With
SPDLitispossibletoexpresscomplexperformanceandreliabilityrequirementsandtoau-
tomaticallyverifythem.ThelogicSPDLallowsthespecificationofrequirementsbymeans
ofextendedregularexpressions,therebyconserving anabstractandaction-oriented view
on the system’s behaviour. The extensions of regularexpressions SPDL provides,make it
possible to apply programming language constructs such as if-then-else and while. This
allowsthespecificationandverificationofverycomplexrequirements.
To compute performance and reliability requirements the data structures that are ap-
pliedto representthe system’s SLTSmust allow efficientnumericalcomputations. To this
end,weapplytheMTBDDbasednumericalalgorithmsthataredescribedin[121].
In the tool CASPA we have implemented both the novel semantics for SPA and the
modelcheckingalgorithmsforSPDLanddemonstratetheirefficiencybyanumberofcase
studies.Contents
PartI IntroductionandFoundations
1 Introduction ............................................................... 1
1.1 Motivation ............................................................ 1
1.1.1 ChoiceofSpecificationLanguage ................................. 3
1.1.2 ModellingofComplexSystems................................... 4
1.1.3 SpecificationofQualitativeandQuantitativeMeasures............. 6
1.2 ContributionsoftheThesis ............................................. 9
1.2.1 CompositionalSymbolicSemantics ............................... 10
1.2.2 AutomaticVerificationofStochasticSystems ...................... 11
1.3 RelatedWork.......................................................... 12
1.3.1 SymbolicSemanticsforProcessAlgebras.......................... 13
1.3.2 TemporalLogics................................................. 13
1.4 Outline ............................................................... 14
2 Foundations ............................................................... 17
2.1 Continuous-TimeMarkovChains ....................................... 17
2.1.1 TransientAnalysis............................................... 19
2.1.2 TheUniformisationMethod...................................... 19
2.1.3 SteadyStateAnalysis ............................................ 21
2.2 BooleanandPseudo-BooleanFunctions ................................. 22
2.2.1 BooleanAlgebra ................................................ 22
2.2.2 BooleanFormulae ............................................... 24
2.2.3 SwitchingFormulae ............................................. 24
2.3 BinaryDecisionDiagrams .............................................. 25
2.3.1 Motivation...................................................... 25
2.3.2 RepresentationofBooleanFormulae .............................. 25
2.3.3 RepresentationofBooleanFormulaeasGraphs-BDDs............. 27
2.3.4 BasicBDDAlgorithms ........................................... 33
2.3.5 ExtendingBDDstoRepresentPseudo-BooleanFormulae ........... 39
2.3.6 RepresentingTransitionSystemsbyBinaryDecisionDiagrams...... 40
2.4 ProcessAlgebras....................................................... 43
2.4.1 Syntax,Semantics,andBisimulationforLOTOS ................... 44
2.4.2 Syntax,Semantics,andEquivalenceforYAMPA.................... 49
2.5 TheLogicPDL......................................................... 52X Contents
2.5.1 SyntaxofPDL................................................... 52
2.5.2 SemanticsofPDL ............................................... 53
2.6 TheLogicCTL......................................................... 55
2.6.1 Introduction .................................................... 55
2.6.2 SyntaxandSemantics............................................ 55
2.7 TheLogicCSL......................................................... 56
2.7.1 State-LabelledContinuous-Time MarkovChains................... 56
2.7.2 SyntaxandSemanticsofCSL..................................... 58
2.7.3 ModelCheckingCSL ............................................ 60
2.7.4 Markov-APBisimulation......................................... 62
PartII SemanticsandVerificationofStochasticProcessAlgebras
3 SymbolicSemanticsforStochasticProcessAlgebras ......................... 65
3.1 Introduction........................................................... 65
3.2 SymbolicDenotationalSemanticsforYAMPA ............................ 66
3.2.1 GeneralIdea .................................................... 67
3.2.2 SemanticRules.................................................. 68
3.2.3 ParallelComposition atArbitraryLevels .......................... 73
3.2.4 Example........................................................ 75
3.3 CorrectnessofSemantics .....................................