Model-Based Testing - AAU PDF Free Download

1y ago

17 Views

1 Downloads

4.62 MB

62 Pages

Report/dmca

Download PDF

Transcription

Model-Based Testingapplied to a Wireless Sensor Network NodeJan TretmansEmbedded Systems Institute, Eindhoven, NLand Radboud University, Nijmegen, NLwith support from:Marcel VerhoefFrits vd WaterenAxel BelinfanteFeng ZhuJulien SchmaltzQuasimodoChessChessUniversity of TwenteRadboud UniversityOpen University NLQuasimodo1

Overview1. The Challenge: A Wireless Sensor Network Node2. Model-Based Testing3. Un-Timed Model-Based Testing with Labelled Transition Systems4. Real-Time Model-Based Testing with Timed Automata5. Model-Based Testing Tools6. Back to the Challenge: The Wireless Sensor Network Node7. Demo8. Concluding RemarksQuasimodo2

The Challenge:A Wireless Sensor Network NodeQuasimodo3

Wireless Sensor Networkswarehouses:sense servationhealth care: on-body networksQuasimodo4

Myrianed: a WSN with Gossipinginspired by biology:ant coloniesand also by girls:cell interactionmessage exchange by gossiping:local communication, global effectQuasimodo5

Myrianed: a WSN with Gossiping Communication inspiredon biology and humaninteraction Epidemic communication Analogy: spreading arumor or a virus MYRIANED “GOSSIP” protocol RF broadcast (2.4 Ghz ISM)Quasimodo6

Myrianed1024 node experimentRF TRANCEIVER(NORDIC SEMI)CPU(ATMEL XMEGA128)RF ANTENNAI/O INTERFACESQuasimodo16

WSN as an Integration ProblemWireless Sensor Network integrating interactingcomponents nodes many: 1000 identical– but third-party nodes? nodes interact using gMAC protocol(gossip Medium Access Control)Quasimodo17

WSN Integration: Model-Based1. define interface–gMACgMAC protocol(gossip Medium Access Control)2. verify gMAC protocol–using Timed Automata and UPPAAL–defects found and repairedAgMCgMAC3. ACgMACprotocolprotocol–Quasimodoalso third-party nodes18

gMAC BehaviourNode 1Node 2Node 3Node 4Node 5Message:Quasimodo2 bytes slot nrtotal 32 bytes19

WSN: Model-Based TestingModel-based testing of a single node: protocol conformance testof the gMAC protocol according to ISO 9646 local test method time is important in gMAC:real-time model-based testingQuasimodo20

Model-Based TestingQuasimodo21

Developments in Testing 11. Manual testingSUTSystem Under Testpass failQuasimodo22

Developments in Testing 2testTTCNcases1. Manual testing2. Scripted testingtestexecutionSUTpass failQuasimodo23

Developments in Testing testexecutionSUT1. Manual testing2. Scripted testing3. Model-basedtestingpass failQuasimodo24

Validation, Verification, and odelpropertiestestingtestingSUTQuasimodo25

Un-Timed Model-Based Testingwith Labelled Transition SystemsQuasimodo26

Approaches to Model-Based TestingSeveral modelling paradigms: Finite State Machine Pre/post-conditions LabelledTransitionSystemsLabelledTransitionSystems Programs as Functions Abstract Data Type testing TimedTimedAutomataAutomata .Quasimodo27

Models: Labelled Transition SystemsLabelled Transition System:〈 S, LI, LU, T, s0 〉initial statestatestransitionsinput actionsoutput actions? input! output!coffee?coin?button!alarm?buttonQuasimodo28

Model-Based TestingSUT passes testssystemmodelSUTconforms tomodel SUTconforms xecutionSUTpass failQuasimodo29

MBT with Labelled Transition Systems SUT ioco modelSUT passes outputconformanceset ofLTS testsLTStestexecutioniocoSUTpass failQuasimodo30

Conformance: ioco def σ Straces (s) : out (i after σ) out (s after σ)i ioco sp δpStraces ( s )p after σ !x LU {τ} . p { σ ( L {δ} )* s{ p’ pσout ( P ) { !x LU p !xQuasimodo!xσ}p’ }, p P } { δ pδp, p P }31

Conformance: iocoi ioco s def σ Straces (s) : out (i after σ) out (s after σ)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 δ )Quasimodo32

Example: a!choc33

Test Generation Algorithm: iocoAlgorithm 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?yallowed outputs?xθfail fail?x!at ( S after !x )fail failt ( S after !x )Quasimodot ( S after ?a )allowed outputs (or δ):!x out ( S )forbidden outputs (or δ): !y out ( S )34

MBT with Labelled Transition Systemssound SUT ioco model exhaustiveSUT passes outputconformanceset ofLTS testsLTStestexecutioniocoSUTbehaving asinput-enabled LTSpass failQuasimodo35

Real-Time Model-Based Testingwith Timed AutomataQuasimodo36

Untimed MBT: iocospecificationtest case? money? button1! money? button2! button1ϑ? tea! tea! coffee?coffeepassQuasimodofailfail37

Real-Time MBTspecificationtest case? money! money @ 5 sec? button1c : 0? button2c : 0c 10c 15[ c 8 ] - ! tea[ c 5 ] - ! coffee! button1 @ 5 sec? tea sutsutrtioco? m ϑs?coffeepassQuasimodofailfail38

Real-Time Model-Based Testing Approach:Extension of LTS:Timed LTSExtension of ioco:real-time ioco Challenges: Is time input or output ? Quiescence: How long is there never eventually no output? Literature: Nielsen, Mikucionis, Skou, Larsen Krichen, Tripakis Brandán Briones, Brinksma Bohnenkamp, Belinfante Khoumsi, Jéron, Marchand Schmaltz, Tretmans39

Untimed Model-Based Testing?but2?but1?but2LTS : 〈 Q , LI , LU , T , q0 〉?but1Observable actions: LI , LU!coffeeSpecifications are LTS?but1?but2Implementations are assumed?but!coffee!teato behave as input-enabled LTSImplementation relation: iocospec40

Timed Input-Output Transition Systems?butc: 0TIOTS : 〈 Q, LI, LU, R 0, T, q0 〉c 10!coffeec 5Observable actions: LI, LUdelay d R 0Specifications are Timed LTSImplementations are assumedto behave as input-enabled Timed LTS41

Some Timed Implementation Relationsi ioco s def σ traces (s) : out (i after σ) out (s after σ) tiocoX?42

A Timed Implementation Relationi ioco s def σ traces (s) : out (i after σ) out (s after σ) rtiocottracesaftertoutRδ(p) ttraces ( s ) { σ ( L R 0 )* soutR ( p ) { x LU R 0 pp aftert σ { p’ pσσx}}p’, σ ( L R 0 )* }43

rtioco?butc: 0rtiococortio?butc 7!coffeec: 0c 9c 7?but!coffeec 3?butc: 0c: 0c 10!coffee?butc: 0c 9!coffeec 5c 7ocort irtiocotrue44

Test Generation Algorithm: rtiocoAlgorithm to generate a test case t(S)from a timed transition systemApply the following steps recursively, non-deterministically:1end test case3observe all outputspassforbidden outputs2supply input !aforbidden outputs?yc 0 allowed outputs?x!a@0?yc dallowed outputs?xdfail failt ( S after !x )fail failallowed outputs (or d):t ( S after !x )t ( S after ?a )!x out ( S )forbidden outputs (or d): !y out ( S )45

Model-Based Testing ToolsQuasimodo46

Some MBT Tools AETG MaTeLo Agatha Phact/The Kit TestGen (Stirling) Agedis QuickCheck TestGen (INT) Autolink Reactis TestComposer ConformiqQtronic RT-Tester TGV SaMsTaG TorX Cooper SmartestingTest Designer TorXakisTorXakis T-Vec Uppaal-CoverQ G st Spec Explorer Uppaal-TronTron Gotcha Statemate Tveda JTorXJTorX STG .uasimodo47

Tron, JTorX, TorXakis: On-the-Fly MBT On-the-fly test generation and test execution Implementation relation: (rt)ioco Mainly applicable to reactive systems / state based utSUTobserveoutputpassfailinconclusiveQuasimodo48

Back to the Challenge:The Wireless Sensor Network NodeQuasimodo49

WSN Node in Protocol Layersnode 1ApplicationUpper ayerRadioLowerLayerTesternode 2node rRadioLayerRadioLayerMedium LayerQuasimodo51

Local Test MethodUpper terfaceLower TesterSoftwareFirst approach: only software, on host simulated, discrete timeQuasimodoif(gMacFrame.currentSlotNumber gMacFrame.lastFrameSlot) {gMacFrame.currentSlotNumber 0;gMacFrame.syncState gMacNextFrame.syncState;if (semaphore.appBusy 1) {mcTimerSet(SLOT TIME);mcPanic(MC FAULT APPLICATION);return;52}

WSN: Test ArchitectureUpper TesterModel-BasedTest Tool:AdapterGMAC layer:Softwaresockets transformmessages synchronizesimulatedtime Uppaal-Tronsockets JTorX TorXakisLower TesterQuasimodo53

WSN: Model-Based Testingtest esgenerationUppaal-TronTA modelsystemmodelrtiocotestexecutionadapterpass failQuasimodoSUTWSN softwareon PC(vague)descriptionsguruad-hoc modellearning54

WSN: Test-Based Modelingtest runspass failQuasimodoMake a esgenerationJTorXsystem?modeladapterSUTfrom observationsmade during testingWSN softwareon PC55

WSN: A Timed Automaton ModelQuasimodo56

DemoQuasimodo57

Concluding RemarksQuasimodo58

Quasimodo Model-Based Testing CasesQuasimodo Chess: WSN gMAC protocol Hydac: model-based testing of existing controller for safety Terma: Modular Multi-Spectral Imaging Array NovoNordisk: off-line testing Dutch electronic biometric passport InterNLnet: Automated trust Anchor Updating in DNSSECQuasimodo59

MBT Lessons Model construction– leads to detection of design and specification errors– how to get a valid model? 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, .Quasimodo60

MBT PerspectivesModel based formal testing can improve the testing process : model is precise and unambiguous basis for testing– design errors found during validation of model longer, cheaper, more flexible, and provably correct tests– easier test maintenance and regression testing automatic test generation and execution– full automation : test generation execution analysis extra effort of modelling compensated by better tests– is modelling really an extra effort? (commercial) model-based testing tools become availableQuasimodo61

Thank you !Quasimodo62

Q 1 Model-Based Testing applied to a Wireless Sensor Network Node Jan Tretmans Embedded Systems Institute, Eindhoven, NL and Radboud University, Nijmegen, NL