Games and Scenarios for Real-Time System Validation

Shuhao Li

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

Resumé

Denne afhandling omhandler forskning i validering af realtidsbaserede indlejrede software-systemer i forbindelse med modelbaseret udvikling. Afhandlingen præsenterer scenariebaserede og spilteoretiske tilgange til systemanalyse, verificering, syntese samt testning for derved at kunne håndtere de udfordringer, der opstår ved systemkarakteristika for ukontrollerbare miljøer, komplekse procesinteraktioner, kvantitative tidsrestriktioner, partiel observerbarhed og kombinationer heraf.

En udvidelse af live sequence charts (LSC) med tid præsenteres, således at indbyrdes procesadfærd og scenariebaserede krav til samtidige og kommunikerende realtidssystemer kan modelleres og specificeres i LSC. Ved at oversætte LSC til tidsautomater (TA), reduceres verifikation af konsistens af scenariebaserede modeller samt verifikation af egenskaber for disse til verifikation af CTL-egenskaber for realtidssystemer. Ligeledes reduceres syntese af eksekverbare systemer fra scenariebaserede modeller til at løse tidsafhængige spil. Ved at anvende vores prototypeoversætter i samspil med modelverifikationsværktøjet Uppaal og værktøjet Uppaal-Tiga, som anvendes til at finde løsninger til spil, påvises det, at disse metoder kan bidrage til at sikre korrekt interaktion for tidlige systemdesign, samt at disse opfylder eventuelle tidskrav.

Afhandlingen viser endvidere, at systematisk gennemprøvning (testning) af reaktive realtidssystemer kan ses som et tidsafhængigt spil mellem testudføreren og systemet som afprøves. Derfor præsenteres metoder, hvori vindende strategier anvendes som test-cases for black-box conformance testing. Disse metoder generaliseres til at imødekomme problemstillinger, der kun giver anledning til muligt vindende strategier. I disse tilfælde er den fortsatte afprøvning baseret på kooperative vindende strategier, der kræver samarbejde fra systemet tidligt i spillet. Endvidere tilpasses metoderne til tilfælde, hvor kun partiel observerbarhed haves, dvs. hvor kun ufuldstændige oplysninger fås fra systemet. Alle disse metoder bidrager til i højere grad at kunne teste for korrekt reaktion ved stimuli og rettidige reaktioner fra de pågældende systemer. Eksperimentelle evalueringer gennem case-studies indikerer, at de foreslåede metoder er realistiske -- både konceptuelt, algoritmisk og med hensyn til beregnelighed.
OriginalsprogEngelsk
Udgivelses stedAalborg
ForlagInstitut for Datalogi, Aalborg Universitet
Vol/bind57
Antal sider224
ISBN (Trykt)1601-0590
StatusUdgivet - 19 apr. 2010

Fingerprint

Real time systems
Observability
Model checking
Testing
Systems analysis
Embedded software

Emneord

  • Realtidssystemer
  • Indlejrede Systemer
  • Validering
  • Scenarier
  • Live Sequence Charts (LSCs)
  • Konsistens
  • Syntese
  • Tidsmærkede Transitionsystemer (TLTS)
  • Tidsautomater (TA)
  • Tidsspil
  • Tidsspilsautomater (TGA)
  • Kontrolsyntese
  • Strategier
  • Modelbaseret Testning
  • Test-Cases

Citer dette

Li, S. (2010). Games and Scenarios for Real-Time System Validation. Aalborg: Institut for Datalogi, Aalborg Universitet.
Li, Shuhao. / Games and Scenarios for Real-Time System Validation. Aalborg : Institut for Datalogi, Aalborg Universitet, 2010. 224 s.
@phdthesis{4764ff30eb1711deb63d000ea68e967b,
title = "Games and Scenarios for Real-Time System Validation",
abstract = "This thesis presents research on the validation of real-time embedded software systems in the context of model-based development. The thesis proposes scenario-based and game-theoretic approaches to system analysis, verification, synthesis and testing to address the challenges that arise from the system characteristics of environment uncertainties, complex process interactions, quantitative timing constraints, partial observability and combinations thereof.We make timed extensions to live sequence chart (LSC) such that the inter-process behaviors and scenario-based requirements of concurrent communicating real-time systems can be modeled and specified with LSC. By translating LSC to timed automata (TAs), we reduce scenario-based model consistency checking and property verification to CTL real-time model checking problems, and reduce scenario-based synthesis to a timed game solving problem. By linking our prototype translators with existing model checker Uppaal and game solver Uppaal-Tiga, we show that these methods contribute to the interaction correctness and timeliness of early system designs. The thesis also shows that testing a real-time reactive system can be viewed as playing a timed game between the tester and the system under test (SUT). We propose methods of using winning strategies as test cases for black-box conformance testing. The methods are generalized to problems where only possibly winning game strategies can be obtained. In this case continued testing requires some early-stage ``cooperations'' from the SUT. Furthermore, we adapt the methods to the partial observability settings where only imperfect information about the SUT is available. All these methods contribute to the improved ability to test for reactivity correctness and timeliness of the systems in question. Experimental evaluations with case studies indicate that the proposed approaches are conceptually, algorithmically and computationally viable.",
keywords = "Realtidssystemer, Indlejrede Systemer, Validering, Scenarier, Live Sequence Charts (LSCs), Konsistens, Syntese, Tidsm{\ae}rkede Transitionsystemer (TLTS), Tidsautomater (TA), Tidsspil, Tidsspilsautomater (TGA), Kontrolsyntese, Strategier, Modelbaseret Testning, Test-Cases, Real-Time Systems, Embedded Systems, Validation, Scenarios, Live Sequence Charts (LSCs), Consistency, Synthesis, Timed Labeled Transition Systems (TLTS), Timed Automata (TAs), Timed Games, Timed Game Automata (TGAs), Controller Synthesis, Strategies, Model-Based Testing, Test Cases",
author = "Shuhao Li",
year = "2010",
month = "4",
day = "19",
language = "English",
isbn = "1601-0590",
volume = "57",
publisher = "Institut for Datalogi, Aalborg Universitet",
address = "Denmark",

}

Li, S 2010, Games and Scenarios for Real-Time System Validation. bind 57, Institut for Datalogi, Aalborg Universitet, Aalborg.

Games and Scenarios for Real-Time System Validation. / Li, Shuhao.

Aalborg : Institut for Datalogi, Aalborg Universitet, 2010. 224 s.

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

TY - BOOK

T1 - Games and Scenarios for Real-Time System Validation

AU - Li, Shuhao

PY - 2010/4/19

Y1 - 2010/4/19

N2 - This thesis presents research on the validation of real-time embedded software systems in the context of model-based development. The thesis proposes scenario-based and game-theoretic approaches to system analysis, verification, synthesis and testing to address the challenges that arise from the system characteristics of environment uncertainties, complex process interactions, quantitative timing constraints, partial observability and combinations thereof.We make timed extensions to live sequence chart (LSC) such that the inter-process behaviors and scenario-based requirements of concurrent communicating real-time systems can be modeled and specified with LSC. By translating LSC to timed automata (TAs), we reduce scenario-based model consistency checking and property verification to CTL real-time model checking problems, and reduce scenario-based synthesis to a timed game solving problem. By linking our prototype translators with existing model checker Uppaal and game solver Uppaal-Tiga, we show that these methods contribute to the interaction correctness and timeliness of early system designs. The thesis also shows that testing a real-time reactive system can be viewed as playing a timed game between the tester and the system under test (SUT). We propose methods of using winning strategies as test cases for black-box conformance testing. The methods are generalized to problems where only possibly winning game strategies can be obtained. In this case continued testing requires some early-stage ``cooperations'' from the SUT. Furthermore, we adapt the methods to the partial observability settings where only imperfect information about the SUT is available. All these methods contribute to the improved ability to test for reactivity correctness and timeliness of the systems in question. Experimental evaluations with case studies indicate that the proposed approaches are conceptually, algorithmically and computationally viable.

AB - This thesis presents research on the validation of real-time embedded software systems in the context of model-based development. The thesis proposes scenario-based and game-theoretic approaches to system analysis, verification, synthesis and testing to address the challenges that arise from the system characteristics of environment uncertainties, complex process interactions, quantitative timing constraints, partial observability and combinations thereof.We make timed extensions to live sequence chart (LSC) such that the inter-process behaviors and scenario-based requirements of concurrent communicating real-time systems can be modeled and specified with LSC. By translating LSC to timed automata (TAs), we reduce scenario-based model consistency checking and property verification to CTL real-time model checking problems, and reduce scenario-based synthesis to a timed game solving problem. By linking our prototype translators with existing model checker Uppaal and game solver Uppaal-Tiga, we show that these methods contribute to the interaction correctness and timeliness of early system designs. The thesis also shows that testing a real-time reactive system can be viewed as playing a timed game between the tester and the system under test (SUT). We propose methods of using winning strategies as test cases for black-box conformance testing. The methods are generalized to problems where only possibly winning game strategies can be obtained. In this case continued testing requires some early-stage ``cooperations'' from the SUT. Furthermore, we adapt the methods to the partial observability settings where only imperfect information about the SUT is available. All these methods contribute to the improved ability to test for reactivity correctness and timeliness of the systems in question. Experimental evaluations with case studies indicate that the proposed approaches are conceptually, algorithmically and computationally viable.

KW - Realtidssystemer

KW - Indlejrede Systemer

KW - Validering

KW - Scenarier

KW - Live Sequence Charts (LSCs)

KW - Konsistens

KW - Syntese

KW - Tidsmærkede Transitionsystemer (TLTS)

KW - Tidsautomater (TA)

KW - Tidsspil

KW - Tidsspilsautomater (TGA)

KW - Kontrolsyntese

KW - Strategier

KW - Modelbaseret Testning

KW - Test-Cases

KW - Real-Time Systems

KW - Embedded Systems

KW - Validation

KW - Scenarios

KW - Live Sequence Charts (LSCs)

KW - Consistency

KW - Synthesis

KW - Timed Labeled Transition Systems (TLTS)

KW - Timed Automata (TAs)

KW - Timed Games

KW - Timed Game Automata (TGAs)

KW - Controller Synthesis

KW - Strategies

KW - Model-Based Testing

KW - Test Cases

M3 - Ph.D. thesis

SN - 1601-0590

VL - 57

BT - Games and Scenarios for Real-Time System Validation

PB - Institut for Datalogi, Aalborg Universitet

CY - Aalborg

ER -

Li S. Games and Scenarios for Real-Time System Validation. Aalborg: Institut for Datalogi, Aalborg Universitet, 2010. 224 s.