2012 · 106 citations · 13 references
EngineeringAutomotive EngineeringComputer ScienceFormal MethodsReal-time SystemsSystems ModelingFunctional VerificationModel CheckingReal-time ControlReal-time Systems DesignSpecification LanguagesTemporal LogicReal-time Systems VerificationReal-time Temporal LogicTemporal Logic AssertionsTemporal Logic ReasoningTemporal Logic SpecificationTemporal Logic VerificationTemporal SpecificationsTemporal Verification
S-TALIRO is a software toolbox that performs stochastic search for system trajectories that falsify realtime temporal logic specifications. S-TaLiRo is founded on the notion of robustness of temporal logic specifications. In this paper, we present a dynamic programming algorithm for computing the robustness of temporal logic specifications with respect to system trajectories. We also demonstrate that typical automotive functional requirements can be captured and falsified using temporal logics and S-TALIRO.
13
Specifying real-time properties with metric temporal logic
Ron Koymans · Real-Time Systems · 1990 · 1.2K citations
Taming heterogeneity - the Ptolemy approach
Johan Eker, Jörn W. Janneck, Edward A. Lee et al. · Proceedings of the IEEE · 2003 · 1.1K citations