NEWS! We won an IBM Eclipse Innovation Grant 2005, so there will be a VInTiMe plugin for Eclipse. Read more here. 
VInTiMe: Combining HighLevel Finesse with LowLevel Muscle 


VInTiMe (Verifier of INtegrated TImed ModEls) [ABGKOS04] is a suite of tools that combines highlevel expressive power, unassisted propertypreserving modelreduction and lowlevel distributed model checking power to describe and verify complex RealTime Systems designs and their properties. VInTiMe comprises the integration of the tools Lapsus, VTS, ObsSlice and Zeus. Lapsus [BF99, Br00] translates realtime system designs based on fixedpriority scheduling into timed automata. Succinctly, it uses WorstCase Completion Times (WCCT) and bestcase completion times (BCCT) –which can be calculated using analytical techniques provided by those theories– to build an abstract and analyzable model of the system based on timed automata. VTS [ABKO04, home page] is a notation for expressing realtime requirements in a visual and friendly, yet powerful, language, by means of negative scenarios. A VTS scenario is basically an annotated partial order of relevant events, denoting a (possibly infinite) set of matching timestamped executions. VTS is meant to existentially predicate on system executions. ObsSlice [BGO04, home page] is an optimization tool suited for the verification of networks of timed automata using virtual observers, the same kind of observers that VTS produces. It automatically discovers the set of modeling elements that can be safely ignored at each location of the observer by synthesizing behavioral dependence information among components. ObsSlice is fed with a network of timed automata and generates a transformed network which is equivalent to the one provided, up to branchingtime observation. Zeus: [BOS03, BOS04] is a distributed model checker that evolves from KRONOS. As such, it works over models expressed in terms of timed automata, being its main features a rigorous correctness proof for its distributed algorithm, and a high degree of flexibility due to its software architecture approach. 