Abstrakt. Probabilistisk modellkontroll är en automatisk formell verifieringsteknik för analys av kvantitativa egenskaper hos system som uppvisar stokastiskt beteende. PRISM är ett probabilistiskt modellkontrollverktyg som redan framgångsrikt har använts inom ett brett spektrum av tillämpningsområden, från kommunikationsprotokoll i realtid till biologiska signalvägar. Verktyget har nyligen genomgått en betydande utveckling. Viktiga tillägg inkluderar faciliteter för att manuellt utforska modeller, Monte-Carlo diskreta simuleringstekniker för ungefärlig modellanalys (inklusive stöd för distribuerad simulering) och förmågan att beräkna kostnads- och belöningsbaserade åtgärder, t.ex. "den förväntade energiförbrukningen i systemet innan det första felet inträffar". I detta dokument ges en översikt över PRISM:s alla huvuddrag. Mer information finns på webbplatsen: www.cs.bham.ac.uk/.dxp/prisma. Probabilistisk modellkontroll är en automatisk formell verifieringsteknik för analys av system som uppvisar stokastiskt beteende. Exempel på sådana system är välkända kommunikationsprotokoll som FireWire och Bluetooth, som använder randomisering, och ett brett spektrum av dator- och kommunikationssystem, vars oförutsägbara egenskaper, t.ex. meddelandeförseningar eller tidpunkter för misslyckande, bäst representeras på ett probabilistiskt sätt. Liksom traditionell modellkontroll innebär denna teknik, från en beskrivning i någon formalism på hög nivå, en ändlig-state-modell av ett verkligt system, men dessutom inklusive information om sannolikheten och tidpunkten för övergångar mellan stater som inträffar. Ur denna modell kan ett brett spektrum av kvantitativa mått i det ursprungliga systemet beräknas automatiskt. PRISM är ett probabilistiskt modellkontrollverktyg som redan har använts för att tillämpa dessa tekniker på en stor och mångfaldig uppsättning fallstudier. I följande avsnitt beskriver vi de typer av probabilistisk modell som stöds av PRISM och egenskaperna hos dessa modeller som kan analyseras. Vi ger sedan en översikt över de viktigaste funktionerna i verktyget. Slutligen sammanfattar vi de fallstudier som verktyget redan har tillämpats på och de olika resurser som finns tillgängliga.
Probabilistisk modellkontroll REF är en förlängning av modellkontroll [1] som ursprungligen utvecklades som en formell teknik för att hitta fel i kretsar.
PRISM: A tool for automatic verification of probabilistic systems
{'venue': 'Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), volume 3920 of LNCS', 'journal': None, 'mag_field_of_study': ['Computer Science']}