WIXLIB

Model-Based Testing :The Test of Formal ModelsJan TretmansESI& Radboud University Nijmegen

Testing(Software) Testing:checking or measuringsome quality characteristicsof an executing objectby performing experimentsin a controlled wayw.r.t. a specificationspecificationtesterSUTSystem Under Test2

Towards Model-Based Testing Increase in complexity, and quest for higher quality software– testing effort grows exponentially with system size– testing cannot keep pace with development More abstraction– less detailSoftware bugs / errors cost US economy yearly: 59.500.000.000 (www.nist.gov) 22 billion could be eliminated – model-based development; OMG’s UML, MDA, Simulink/Matlab Checking quality– practice: testing - ad hoc, too late, expensive, lot of time– research: formal verification - proofs, model checking, . . .with disappointing practical impact3

Testing ComplexityIncrease of complexity and size of systemstesting effort grows exponentially with system sizetesting cannot keep pace with developmentx : [0.9]10 ways that it can go wrong10 combinations of inputs to checkx : [0.9]y : [0.9]y : [0.9]x : [0.9]z : [0.9]100 ways that it can go wrong100 combinations of inputs to check1000 ways that it can go wrong1000 combinations of inputs to checkAutomation of testing is necessary.Model-based testing is one of the techniques4

Developments in Testing 11. Manual testingSUTSystem Under Testpass fail5

Developments in Testing 2testTTCNcases Manual testing Scripted testingtestexecutionSUTpass fail6

Developments in Testing 3high-leveltest notation Manual testing Scripted testing Test-modelbased testingtestexecutionSUTpass fail7

Developments in Testing 4 Manual testing Scripted testing Test-modelbased testing rationsystemmodeltestexecutionSUTpass fail8

Model-Based TestingSUT passes testssystemmodelSUTconforms tomodel SUTconforms xecutionSUTpass fail9

Model-Based Testing Model Based Testing– testing of SUT with respect to a (formal) model / specification:state/transition model, pre/post conditions, CSP,Promela, UML, Spec#, . . . . Promises better, faster, cheaper testing– algorithmic generation of tests and test oracles : tools– formal and unambiguous basis for testing– measuring the completeness of tests– maintenance of tests through model modification– potential to combine practice - testing and theory - formal methods10

Validation, Verification, and Testinginformalrequirementsinformal worldvalidationmodelverificationtestingreal worldrealization11

Doing Something Else with Models Modellingmaking a model reveals errors Simulationgo step-by-step through the model Model checkinggo through all states of the model Provingprove theorems about the model Code generationexecutable code from the model Model mininggenerate a model from observation12

Code Generation from a ModelA model is more (less)metthan code generation: views abstraction testing of aspects verification and validationof aspects13

Approaches to Model-Based TestingSeveral modelling paradigms: Finite State Machine Pre/post-conditions LabelledLabelled TransitionTransition SystemsSystems Programs as Functions Abstract Data Type testing Timed Automata .14

LTS Model for E-Passport15

Models and Models of Test Casesspecificationmodeltest casemodel? reset? BAC CALL! AA NOK! reset? AA Call! BAC CALL! BAC OKϑ? BAC OK?BAC NOKpassfail? .failfail16

Model-Based TestingSUT passes testssystemmodelSUTconforms tomodel SUTconforms xecutionSUTpass fail17

MBT with Labelled Transition SystemsLTS-basedtestgeneration SUT ioco modelSUT passes testsset ofLTS teststestexecutionLTSmodelinput/outputconformance: iocoSUTbehaving as LTSpass fail18

Correctness: ioco def σ Straces (s) : out (i after σ) out (s afteri ioco sσ)pδpStraces ( s )p after σ !x LU {τ } . p { σ ( L {δ } )* s{ p’ pout ( P ) { !x LU pσ!x!xσ}p’ }, p P } { δ pδp, p P }19

Example: dime?dime?dime!tea!coffeeiocoδ!coffee!tea!choc20

Example: iocospecificationmodel? x (x 0)implementationmodels (SUT)? x (x 0)? x (x 0)! x?x!y(y x y x)? x (x 0)LTS and ioco allow: non-determinism the specification of properties!error? x (x 0) under-specification! - x?xrather than construction21

Test Generation AlgorithmAlgorithm to generate a test case t(S)from a transition system state set S, with S ( initially S s0 afterε ).Apply the following steps recursively, non-deterministically:1end test case3observe all outputspassforbidden outputs2?ysupply input !aallowed outputsforbidden outputs?y?x!aallowed outputs?xθfail failt ( S after !x )fail failt ( S after !x )t ( S after ?a )allowed outputs (or δ):!x out ( S )forbidden outputs (or δ): !y out ( S )22

Test Result Analysis: CompletenessFor every test tgenerated with the ioco test generation algorithm we have: Soundness :t will never fail with a correct implementationi ioco s impliesi passes tExhaustiveness :each incorrect implementation can be detectedwith a generated test ti ioco simplies t : i fails t23

Model-Based Testing ToolsSome Tools for Model-Based testing AETG QuickCheck TestComposer Agatha Reactis TGV Agedis RT-Tester TorX Autolink SaMsTaG TorXakisTorXakis Conformiq Smartesting Uppaal-Tron Cooper Spec Explorer Tveda Cover Statemate . G st STG Gotcha TestGen (Stirling) Phact/The Kit TestGen (INT)24

TorXakis: A Tool for Model-Based Testing On-the-fly test generation and test execution Implementation relation: Mainly applicable to reactive systems / state based veobserveoutputSUT25

Electronic PassportNew Passport Machine Readable Passport ( MRP, E-passport ) with chip (JavaCard), contact-less storage of picture, fingerprints, iris scan, . access to this data protected by encryption and a new protocol just released in EUOur job: testing of e-passports emphasis on access protocol exchange of request-respons messagesbetween passport and reader (terminal)26

E-Passports : Basic ModelINITBACEACBasic Access Control Extended Access Controlinitial protocolrequires successful BACread photoread photoread personal dataread personal dataread fingerprints27

Model-Based Testing of ystemmodeltestexecutionSUTpass fail28

Model-Based Testing of E-Passportsstate-basedmodeltest utionadapterpass failpass failSUTenglishspecificationse-passport& wirelessreader29

MBT for E-Passports : ProcessunderstandingICAO lysisrefinefailSUTpassportmaketestenvironment30

MBT for E-Passports : Results Tested:– Basic Access Control (BAC)– Extended Access Control (EAC)– Active Authentication (AA)– Data Reading: requires data testing Tests up to about 1,000,000 test events– complemented with manual tests No error found yet .31

MBT Lessons Model construction– leads to detection of design and specification errors Adapter/test environment– specific for each system– sometimes laborious, but not specific for MBT Longer and more flexible tests– full automation : test generation execution analysis– easy to repeat for regression testing, modifications, .32

Demo !33

3 Towards Model-Based Testing Increase in complexity, and quest for higher quality software - testing effort grows exponentially with system size - testing cannot keep pace with development More abstraction - less detail - model-based development; OMG's UML, MDA, Simulink/Matlab Checking quality - practice: testing - ad hoc, too late, expensive, lot of time