Ulf Nilsson
Institutionen för datavetenskap
ulfni@ida.liu.se
2002-10-11

Bakgrund

Syftet med området formella metoder är i första hand att (1) erbjuda matematiska verktyg för att formellt modellera, specificera och verifiera egenskaper hos system, helst tidigt i utvecklingsprocessen, samt att (2) erbjuda verktyg och metoder som — så långt detta är möjligt — säkerställer att systemegenskaper bevaras under designprocessen. Ordet "säkerställer" skall här inte tolkas bokstavligt — vissa steg i processen kan och bör inte alltid formaliseras utan bör bygga på informella eller halv-formella steg, men processen bör vara stegvis, rigorös och alla designbeslut bör vara välgrundade. Syftet med formella metoder är alltså att införa rutiner och verktygsstöd för att:
  • undvika att fel introduceras under tidiga utvecklingsfasen, och 
  • om fel ändå uppkommer, se till att felen upptäcks så tidigt som möjligt. 

För att kunna resonera formellt om system och systemegenskaper krävs ett formellt specifikationsspråk (för att beskriva systemegenskaper) och ett modelleringsspråk (för att beskriva själva systemet). Dessa behöver inte vara ett och samma språk — modelleringsspråket kan t.ex. vara en grafisk notation och specifikationsspråket textbaserat. Det är en fördel om modelleringsspråket understödjer abstraktion och förfining och därmed kan användas åtminstone under den tidiga designen av system. Möjligheten till abstraktion är också viktig eftersom vissa typer av egenskaper ibland är enklare att visa innan systemmodellen vuxit och blivit alltför komplex. Detta gäller inte minst om man, som i ett av projekten nedan, vill isolera fel i systemet — det färdiga systemet är ofta så komplext att diagnos blir praktiskt taget omöjlig om man inte utgår från en abstraktion, dvs. en modell av systemet.

Vår forskning inriktas på att utveckla metoder och verktygsstöd för specifikation, design och analys av diskreta dynamiska system innehållande inbyggd programvara. Vi undersöker bland annat hur logikprogram och villkorsprogrammering kan användas för att specificera och modellera dynamisk system. Vi kommer att undersöka om metoder som idag används för analys av programspråk — exempelvis, abstrakt interpretering och programtransformationer — kan kombineras med metoder för systemverifikation. Vi undersöker även hur andra matematiska modeller — exempelvis tillståndsmaskiner och olika former av kalkyler — kan användas för systemmodellering och för att resonera om systemmodeller.

Industriella motiv

Programvara får en allt större betydelse i olika industriella system. Samtidigt saknas bra metoder för att verifiera och validera om den ingående programvaran verkligen gör vad den ska. Testning som är den idag dominerande metoden fungerar acceptabelt för sekvensiella, deterministiska program, men det blir allt vanligare att programvaran är distribuerad eller exekverar parallellt och då är testning inte längre någon tillförlitlig metod eftersom systemet inte längre alltid beter sig deterministiskt - ett system kan mycket väl bete sig som förväntat i hundra testkörningar för att nästa gång, utan synbar anledning, bete sig helt annorlunda. Formell verifikation löser naturligtvis inte alla problem eftersom formell verifikation liksom testning i allmänhet bara kan visa på närvaron av fel — men flera systemegenskaper som inte kan verifieras med hjälp av testning kan visas med formell verifikation. Detta gäller t.ex. säkerhetsegenskaper och vissa tidsegenskaper.

Oerhört mycket tid och pengar läggs idag ner på testning. Den stora nackdelen med testning är dock inte detta, utan att fel inte upptäckas förrän systemet eller systemkomponenten redan utvecklats (i bästa fall). Detta kan naturligtvis leda till stora kostnader i form av felsökning och om-design av systemet. Formell verifikation möjliggör tidig upptäckt av fel. Dessutom understödjer formell specifikation tidig förståelse av problemet och systematisk design av det färdiga systemet. Formella metoder gör det även möjligt att betrakta system på olika abstraktionsnivåer — något som är viktigt både ur dokumentationssynpunkt och för att kunna analysera systembeteenden — i många fall är abstraktion en nödvändighet eftersom det färdiga systemet ofta är alltför komplext.

Trots de uppbara fördelarna med formella metoder finns samtidigt en viss skepticism mot området. En orsak till detta är säkerligen bristen på lättanvända system (även om det börjat dyka upp kommersiella produkter). Men en bidragande orsak är säkerligen också att de formella metoderna är för generella och tar för liten hänsyn till existerande metoder och praktik. Det är därför viktigt att försöka hitta verkliga problem, att studera existerande metoder och att försöka anpassa de formella metoderna till gängse praxis.

Projektbeskrivning

Projektet bedrivs inom TCSLAB (Laboratoriet för Teoretisk Datalogi) vid Institutionen för datavetenskap, Linköpings universitet. Projektet leds av Ulf Nilsson (docent) och omfattar för närvarande en doktorand, Dan Lawesson, och en stipendiat (tilltänkt doktorand), Vladislavs Jahundovics, och består av tre delprojekt.

Delprojekt 1: Verktygsstöd för designgranskning

Detta projekt avslutades formellt augusti 2001 och var ett samarbete med Ericsson SoftLab AB med finansiering från Vinnovas komplexa tekniska system. Syftet med projektet var att understödja tidig upptäckt av fel i reaktiva system inom telekomindustrin. De dominerande metoderna för att upptäcka fel är idag testning och inspektion . Testning kan dock bara användas på ett existerande system eller på en prototyp av systemet, något som leder till att många fel upptäcks sent. Inspektion kan användas tidigare i processen men inspektion är i allmänhet ett manuellt arbete utan annat stöd än checklistor och "style-guides". Doktoranden Tim Heyer beskrev i sin licentiatavhandling hur metoder utvecklade för att formellt bevisa programkorrekthet kan modifieras för att understödja ett mer informellt arbetssätt. Han har bland annat visat hur den modifierade metoden kan användas för att automatiskt generera frågor som kan utnyttjas vid kodgranskning . Sedan april 1999 har vi arbetat med att generalisera dessa ideer så att de kan användas under systemutvecklingens tidigare faser - speciellt vid designgranskning av systemet. Vi har undersökt hur metoderna ska generaliseras för att kunna resonera om en systemdesign i UML (Unified Modeling Language) — en grafisk designnotation baserad på objekt-orienterade principer. Projektet har resulterat i:
  • en designnotation baserad på UMLs sekvens- och klassdiagram [13] ; 
  • en specifikationsnotation baserad på användningsdiagram och OCL (Object Constraint Language ); ett predikatlogiskt språk som ingår i UML och med vars hjälp man kan uttrycka bland att pre- och postvillkor samt olika former av invarianter [12];
  • en metod för att automatiskt generera frågor ur design och specifikation [9,4]; 
  • ett grafiskt prototypverktyg som understödjer modellering i vår delmängd av UML och semi-formella kommentarer av designen med villkor i sprecifikationsspråket, samt automatisk generering av frågor (s.k. verifikationsvillkor).
Tim försvarade sin doktorsavhandling [3] i dec 2001. Arbetet med projektet fortgår dock i reducerad omfattning och i samarbete med Karlstads Universitet, där Tim nu arbetar. Under 2002 har ett examensarbete påbörjats för att utvidga metoden till en större del av UML.

Delprojekt 2: Modellbaserad diagnos av objekt-orienterade styrsystem

Den andra verksamheten bedrivs inom ramen för ISIS i samarbete med ABB Robotics och Reglerteknik vid ISY. Motivationen för projektet är ett styrsystem för industrirobotar som utvecklats vid ABB. Systemet bygger på en objektorienterad arkitektur och är mycket konfigurerbart. Tillsammans leder detta till en dynamisk systemarkitektur där komponenterna endast är "medvetna" om sin omedelbara närhet och där systemfel ofta blir svårdiagnosticerade — feltillstånd leder i allmänhet till propagerande felmeddelanden; felmeddelanden som i händelse av kommunikationsfel inte loggas; och i de fall då meddelanden loggas så är ordningen inte alltid relevant. Arbetet har hittills lett fram till en metod för felisolering baserad på strukturell information som beskriver systemets arkitektur [10,11,15]. I det fortsatta arbetet studerar doktoranden Dan Lawesson hur metoden kan förbättras genom att även ta i beaktande information om systemets dynamiska beteende (som beskrivs med hjälp av UML statecharts). I ett antal artiklar [2,6,7] presenteras hur formella metoder baserade på s.k. model checking kan utnyttjas för att resonera om systemets kausala beroenden genom att reducera dessa till egenskaper som rör den temporala ordningen mellan händelser i systemet.

Dan försvarade sin licentiatavhandling i mars 2001, och beräknas försvara sin doktorsavhandling i slutet av år 2003.

Delprojekt 3: Verifikation

Delprojektet fokuserar på språk och tekniker för att modellera och automatiskt verifiera egenskaper hos programvara och (distribuerade) diskreta system. Bland resultaten kan nämnas:

  • En utvärdering av en existerande metod för designsyntes applicerad på en realtidstillämpning från flygindustrin (på uppdrag av SAAB Dynamics), samt en implementation av metoden i ett logikprogrammeringsspråk med villkorshantering (constraints). Se [16].
  • En ny algoritm för model-checking av temporala egenskaper uttryckta i specifikationsspråket CTL, baserad på beräkningsprinciper från logik och villkorsprogrammeringsområdet. Preliminära resultat indikerar stora tids- och minnes-vinster i vissa fall, men motsatta förhållandet i andra fall [8,14,17].
  • I samarbete med Laurent Fribourg, Ecole Normale Superieure de Cachan/CNRS, har vi utvecklat en metod för semi-automatisk verifikation av så kallade självstabiliserande distribuerade system, dvs system som automatiskt återhämtar sig vid transienta fel trots att ingen enskild process i systemet har kunskap om systemets globala tillstånd. Se [5].
  • I samarbete med P. Dell'Acqua (ITN) och L.M. Pereira (Univ. Lissabon) har vi utvecklat en modell, baserad på logikprogrammering, för asynkrona, uppdaterbara multi-agentsystem [1]; dvs. system av distribuerade processer med förmåga att kommunicera, uppdatera sig själv och andra, generera hypoteser som förklarar observationer vilket, i sin tur, ger möjlighet till rationellt och proaktivt beteende.

Publikationer, avhandlingar och rapporter 1998-2002

  1. P. Dell'Acqua, U. Nilsson, L.M. Pereira. A Logic Based Asynchronous Multi-Agent System. Electronic Notes in Theoretical Computer Science, 70(5), 2002.
  2. Dan Lawesson and Ulf Nilsson and Inger Klein. Fault Isolation using Process Algebra Models. In 13th Intl Workshop on Principles of Diagnosis, DX02. 2002.
  3. T. Heyer. Semantic Inspection of Software Artifacts: From Theory to Practice, Linköping Studies in Science and Technology, PhD Dissertation no 725, 2001.
  4. T. Heyer. Semantic Inspection of UML Designs, Proc. Workshop on Inspection in Software Engineering (WISE'01).  M. Lawford and D.L. Parnas (editors), pp. 58-67, Paris, 2001
  5. M. Duflot, L. Fribourg, U. Nilsson. Unavoidable Configurations of Parameterized Rings of Processes. Proc. of Concurrency Theory (CONCUR'01), Ålborg, Lecture Notes in Computer Science 2154, Springer-Verlag, Aug 2001.
  6. D. Lawesson, U. Nilsson, I. Klein. Model-Checking Based Fault Isolation in UML. In Proc. 12th Intl Workshop on Principles of Diagnosis, DX01, San Sicario, Italy. 2001.
  7. D. Lawesson. Towards Behavioral Model Fault Isolation for Object Oriented Control Systems. Licentiate thesis no 863, 2000.
  8. U. Nilsson, J. Lübcke. Constraint Logic Programming for Local and Symbolic Model-checking . Proc of Int'l Conf. on Computational Logic CL2000, London, Lecture Notes in Artificial Intelligence 1861, Springer-Verlag, 2000.
  9. T. Heyer, Tool Support for Design Inspection: Automatic Generation of Questions. Internrapport, 2000.
  10. M. Larsson and I. Klein and D. Lawesson and U. Nilsson. Fault Isolation in Object Oriented Control Systems . In IFAC SAFEPROCESS 2000, Budapest. June 2000.
  11. M. Larsson, I. Klein, D. Lawesson, U. Nilsson. Model Based Fault Isolation for Object-Oriented Control Systems . Teknisk rapport LiTH-ISY-R-2205, Nov 1999.
  12. T. Heyer, Tool Support for Design Inspection: A Specification Notation . Internrapport, 1999.
  13. T. Heyer, Tool Support for Design Inspection: A Design Notation . Internrapport, 1999.
  14. J. Lübcke, U. Nilsson, On-the-Fly Model Checking of CTL Formulas using Constraint Logic Programming . Intl Workshop on Constraint Programming for Time Critical Applications, Lisbon, 1999.
  15. M. Larsson, I. Klein, D. Lawesson, U. Nilsson. The Need for Fault Isolation in Object-Oriented Control Systems . Technical report LiTH-ISY-R-2098, Feb 1999.
  16. U. Nilsson, S. Streifert, A. Törne, Detailed Design of Avionics Control Software . IEEE Intl Symposium on Real-time Systems, Madrid, 1998.
  17. J. Lübcke, U. Nilsson, CTL Model Checking using Tabled Logic Programs. Workshop on Constraint Programming for Time Critical Applications, Nice, 1998.
Copyright © 1998-2002, Ulf Nilsson