Model-based testing of Real-time systems

Indhold:

Litteratur

  1. Anders Hessel, Kim G. Larsen, Brian Nielsen, Paul Pettersson, and Arne Skou  Time Optimal Test Generation using Uppaal
  2. Kim Larsen, Marius Mikucionis, Brian Nielsen Online testing of real-time systems 
  3. UppAal TRON website 
  4. test opgave
  5. SLIDES

Øvelser

  1.  
    1. Diskutter hvorvidt 1) maskine I er en ioco korrekt implementation af S og 2) om S er en ioco korrekt implementation af I (altså betragt I som specifikation og S som implementation).



    2. Udled test sekvenser LightControlleren, og implementer dem I Java (Kopier og efterlign eksemplerne i filen "TestLightController.java"). Det nemmeste er at kopier kataloget flg. tar fil. Lyscontroller implementationen og lyscontroller testen startes med fx. 
      > java LightController 0
      > java TestLightController localhost 9999 1   for at afvikle test #1 på LightController kørende på samme maskine (sorry kun controller pr maskine, ellers skal I selv ændre LightControllerens port til noget andet og genoversætte.

      Applikationer oversættes med: 
      > javac LightController.java
      > javac TestLightControler.java
    3. Afprøv online test værktøjet UppAal-TRON på LightControlleren. Prøv evt. at seede fejl i LightController.java (oversæt) og se om fejlen fanges.  

      Værktøjet (TIL Solaris+LINUX) er installeret i /user/bnielsen/tuppaal-1.3.1 (kopier til eget hjemmekatalog)
      1. Linux (Marge/Homer)
        • LD_LIBRARY_PATH skal inkludere current dir. eg. (tcsh) "setenv LD_LIBRARY_PATH $LD_LIBRARY_PATH:."
        • make clean
        • make test-lightcontroller  (Kræver at java 1.5 er først i den søge sti (check m kommandoen java -version)).
      2. Solaris (fire1/fire2)
        • LD_LIBRARY_PATH skal inkludere libxml nyere end v 2.6 eg.(tcsh) "setenv LD_LIBRARY_PATH /pack/libxml2-2.6.11/lib:$LD_LIBRARY_PATH:."
        • make clean
        • cp SunOS-5.9-sun4u/gcc-3/tron .
        • unlimit stacksize (sysadm fejl på fire1)
        • make test-lightcontroller  (Kræver at java 1.5 er først i den søge sti (check m kommandoen java -version)).

Med Venlig Hilsen

Arne & Brian