Abstrakt. I detta dokument studerar vi i vilken utsträckning implementering av tidsinställd automata kan uppnås med hjälp av standard semantik och lämplig modellering, istället för att introducera nya semantik. Vi föreslår en genomförandemetod som gör det möjligt att omvandla en tidsinställd automaton till ett program och att kontrollera om genomförandet av detta program på en given plattform uppfyller en önskad egenskap. Detta görs genom att modellera programmet och exekveringsplattformen, respektive, som en oläglig automaton och en samling av tidsinställda automata. Vi studerar också problemet med att bevara egendomen, särskilt när vi flyttar till en "bättre" genomförandeplattform. Vi visar att vissa nyanser uppstår när det gäller definitionen av "bättre", särskilt för digitala klockor. Den grundläggande frågan är att snabbare klockor resulterar i bättre "sampling" och därför kan införa fler beteenden.
Altisen och Tripakis föreslår i REF en genomförandemetod för att omvandla en tidsinställd automaton till ett program, och genom det, kontrollera egenskaper av genomförandet av det programmet.
Implementation of Timed Automata: An Issue of Semantics or Modeling?
{'venue': 'FORMATS', 'journal': None, 'mag_field_of_study': ['Computer Science']}