TUGraz OPEN Library (Graz University of Technology) · 2020 · 14 citations · 4 references
EngineeringComputer EngineeringComputer ScienceFormal MethodsModel-based Systems EngineeringReal-time SystemsFinite State Machine ModelingFinite-state MachinesModel CheckingPredicate LogicTemporal LogicTiming SemanticsAbstract MachinesAbstract State MachinesPredicate Logic SemanticsReal-time System VerificationReal-time Systems VerificationState MachinesSystem Requirements SpecificationTimed Model Checking
We describe a prototype of a simulator for reactive timed abstract state machines (ASM) that checks whether the generated runs verify a requirements specification represented as a formula of a First Order Timed Logic (FOTL). The simulator deals with ASM with continuous or discrete time. The time constraints are linear inequalities. It can treat two semantics, one with instantaneous actions and another one with delayed actions, the delays being bounded and non-deterministic.
4