sess10pr1

Qualitative and Quantitative Analysis of Software Systems:a Model-based View on Integrated Analysis: 

Ed Brinksma University of Twente, Netherlands ISSTA/Wosp Rome, July 24th, 2002 Qualitative and Quantitative Analysis of Software Systems: a Model-based View on Integrated Analysis

MOTIVATION: 

MOTIVATION Can the qualitative and quantitative aspects of reactive systems be modelled and analysed within one compositional framework? Central Issue increasing importance of quantitative behaviour need for integrated design disciplines cross-fertilization theory of approximate correctness

Contents: 

Contents Analysis, validation, and modelling Design, composition, and algebra Model-based test generation Integrated performance analysis Conclusions & perspective

Modelling: 

Modelling science vs. engineering software programs as models models of software systems the role of experimentation

The Empirical Cycle: 

The Empirical Cycle

Methodology of Science: 

Methodology of Science a normative procedure: when is a theory is acceptable? models are refined by iteration models play a descriptive role (Vienna Circle: Carnap et al.)

Engineering: 

Engineering models (specs) are prescriptive deals with artefacts

The Design Cycle: 

The Design Cycle

Methodology of Engineering: 

Methodology of Engineering design cycle is normative, a posteriori artefact is refined by iteration can employ theory of underlying empirical cycles

The formal nature of software: 

The formal nature of software

Programming as mathematics : 

Programming as mathematics programs are formal models of their realizations. program derivation and verification are mathematical activities, subject to proofs validation can be achieved through reliable compilation/interpretation (Dijkstra, Hoare et al.)

Limits of the Mathematical Paradigm: 

Limits of the Mathematical Paradigm incomplete combinatorial explosion large & incomplete unreliable

System Modelling: 

System Modelling specification fragment

System Modelling: 

System Modelling Abstract models of software Interpolation specs and programs Basis for verification Basis for validation like traditional engineering models

System Model Validation: 

System Model Validation Top-down: specification refinement Bottom-up: implementation abstraction Formally: by proof or by construction Empirically: by experimentation

Empirical Validation: 

Empirical Validation analyse

Contents: 

Contents Analysis, validation, and modelling Design, composition, and algebra Model-based test generation Integrated performance analysis Conclusions & perspective

Design and Complexity: 

Design and Complexity Divide and conquer: distribute functionality Hierarchical design: different abstraction levels Modelling formalism must support compositionality and abstraction

Navigating the Design Graph: 

Navigating the Design Graph Abstraction level Alternatives Modelling formalism must support model transformation

Process Algebra: 

Process Algebra abstract process modelling compositionality abstraction transformation laws operational interpretation

Basic Process Algebraic Operators : 

Basic Process Algebraic Operators inaction: 0 action-prefix: a.B , .B choice: B + C , I Bi composition: B ||AC hiding: B \ A definition: p =def B application: p

A very basic example: 

mid |[mid]| hide mid in ||{mid} A very basic example A simple one place buffer Buf =def in . out . Buf Two instances of this buffer Buf out in Buf in out

A very basic example II: 

A very basic example II A two place buffer Buf2 =def in.Half Half =def in.Full + out.Buf2 Full =def out.Half

Equivalence : 

Equivalence Two ways to represent a two place buffer: examples for the need to study equivalences

Equivalence: 

Equivalence Process algebraic equivalences are based on different answers to the question: What is an observable part of the behaviour of a process ? Various notions have been studied (see [van Glabbeek]) trace equivalences testing equivalences bisimulation equivalences

Algebraic Laws: 

Algebraic Laws Equivalences (congruences) induce algebraic laws B + C = C + B (B + C) + D = B + (C + D) B + 0 = B B + B = B B ||A C = C ||A B (B ||A C) ||A D = B ||A (C ||A D)

Expansion Laws: 

Expansion Laws Parallelism can be removed step by step: Let B = k ak .Bk and C = l cl .Cl B ||A C = {ak .(Bk ||A C ) | ak A } + {cl .(B ||A Cl ) | cl A } + {d .(Bk ||A Cl ) | d = ak =cl A } Example: a.0|| c.0 = a.c.0 + c.a.0

Expansion Laws: 

Expansion Laws move between abstraction levels (de)compose functionality stepwise simulation These laws are crucial for the success of process algebraic modelling

Contents: 

Contents Analysis, validation, and modelling Design, composition, and algebra Model-based test generation Integrated performance analysis Conclusions & perspective

Testing With Formal Methods: 

Testing With Formal Methods Advantages formal approach: algorithmic generation of sound tests formal validation of tests tests specification implementation test generator test executor verdict (pass/fail) implements

Correctness Relations: 

Correctness Relations synchronous communication : testing preorder (De Nicola & Hennessy, 1984) conformance preorder (Brinksma 1987) refusal testing (Phillips 1987, Langerak 1990) asynchronous communication : queue-based testing (Brinksma & Tretmans 1992) I/O-based testing (Phalippou,Tretmans,Segala 1993) repetitive quiescence (Tretmans 1996) multiple I/O (Heerink & Tretmans 1997)

Asynchronous Test Contexts: 

( || Env)/A Asynchronous Test Contexts implementation under test test engine operating system test method communication buffers compositionality

Formal Correctness: 

Formal Correctness I ioco S =def   Straces(s): out(I after )  out(S after ) ioco Example: equation solver for y2=x Intuition : I ioco-conforms to S iff if I produces output x after trace , then S can produce x after  if I cannot produce any output after trace , then S cannot produce any output after  (quiescence)

Formal Test Generation: 

Nondeterministic algorithm Generate a test case t(S) from a transition system model with S a set of states (initially S = {s0}) Formal Test Generation Apply the following steps recursively, nondeterministically

Test Generation Example: 

Test Generation Example Equation solver for y2=x Test Note: to cope with non deterministic behaviour, tests are not linear traces, but trees

Validity of Test Generation: 

Validity of Test Generation For every set of tests T generated with the algorithm: Soundness generated test will never fail with ioco-correct implementation I ioco S implies I passes T

Test Generation Tools for ioco: 

Test Generation Tools for ioco TVEDA (CNET - France Telecom) derives TTCN tests from SDL specification developed from practical experiences TGV (IRISA - Rennes) derives tests in TTCN from LOTOS or SDL uses test purposes TorX (Côte de Resyste) on-the-fly test generation and execution uses LOTOS and Promela

TorX Tool Architecture: 

TorX Tool Architecture concentrate on on-the-fly testing

TorX ApplicationHighway Tolling System: 

TorX Application Highway Tolling System

Results: 

Results Test results : Errors found during model validation (design error) and during testing (coding error) Automated testing : beneficial: high volume and reliability very flexible: adaptation and many configurations Real-time : How to cope with real time constraints ? Efficient computation for on-the-fly testing ? Lack of theory: quiescence vs. time-out

Contents: 

Contents Analysis, validation, and modelling Design, composition, and algebra Model-based test generation Integrated performance analysis Conclusions & perspective

Markovian Process Algebra : 

Markovian Process Algebra basic idea: incorporate delays that follow exponential distributions into process algebra MEMORYLESS Two distinct approaches: associate delays to actions TIPP, PEPA, EMPA, ... introduce delays as orthogonal entities IMC (also MLOTOS)

Interactive Markov Chains: 

inaction: 0 prefix: a . B ,  . B choice: B + C or I Bi composition: B ||AC hiding: B \ A or hide A in B definition: p =def B application: p Interactive Markov Chains (). B , inaction: 0 prefix: a . B ,  . B choice: B + C or I Bi composition: B ||AC hiding: B \ A or hide A in B definition: p =def B application: p supports phase type distributions

Algebraic Laws for IMC: 

Algebraic Laws for IMC These are the algebraic laws for strong Markovian bisimulation, a straightforward combination of strong bisimulation and lumpability. B + C = C + B (B + C) + D = B + (C + D) B + 0 = B a.B + a.B = a.B

Interleaving Law: 

Interleaving Law The interleaving law holds for IMC : This does not hold for general distributions!

Queuing Systems in IMC: 

hide enter,serve in CUSTOMER |[enter]| QUEUE(0) |[serve]| SERVER arriving customers queue service clerk Queuing Systems in IMC CUSTOMER =def ( ). enter . CUSTOMER QUEUE(i) =def [i<6]-> enter. QUEUE(i+1) [i>0]-> serve. QUEUE(i-1) SERVER =def serve . ( ) . SERVER

Queuing Systems in IMC: 

hide enter,serve in CUSTOMER |[enter]| QUEUE(0) |[serve]| SERVER Queuing Systems in IMC ?

Queuing Systems in IMC: 

hide enter,serve in CUSTOMER |[enter]| QUEUE(0) |[serve]| SERVER Queuing Systems in IMC

A telephony system: 

A telephony system Original specification developed by P. Ernberg (SICS), further studied in the French/Canadian Eucalyptus project: more than 1500 lines of LOTOS. Extensively verified using state-of-the-art techniques model checking equivalence checking

Performance analysis of the telephony system: 

Performance analysis of the telephony system Takes the original specification without changes. Stochastic delays are incorporated in a compositional way, i.e. as additional constraints imposed on the specification. exponential, Erlang and phase-type distributions. Weak bisimulation is used to factor out nondeterminism. State space >107 leads to a Markov Chain of 720 states with a highly irregular structure. using a dedicated operator, time constraints

Time constraints: 

A particular phone: The time it takes to pick up the phone: The phone with time constraints:  Time constraints 

Analysis results: 

Analysis results 14 different time constraints incorporated. Compositional minimisation to avoid state space explosion. Here: two subscribers phoning each other.

Tools used: 

Tools used CAESAR/ALDEBARAN original specification, first minimisation steps. TIPPtool time constraints, final minimisations, numerical analysis.

Contents: 

Contents Analysis, validation, and modelling Design, composition, and algebra Model-based test generation Integrated performance analysis Conclusions & perspective

Conclusions: 

Conclusions software engineering & analysis need modelling, like in traditional engineering modelling formalisms must support composition, abstraction & transformation process algebra provides theoretical framework & tool support (expansion laws) integrated quantitative & qualitative modelling & analysis by embedding models in specialized contexts (extending theory where needed)

Analytic Contexts: 

Analytic Contexts

Perspectives: 

Perspectives Extending specialized contexts Existing: testing, soft & hard real-time Future: dependability, security Extending scope of analysis techniques Model checking CTMCs (ETMCC tool) Non-Markovian analysis Hard real-time testing (STRESS = TorX + Uppaal) Soft real-time testing Integrated modelling and tool support MoDest language and tools project