High-level Formal Modeling and Analysis of Real-Time and Hybrid Systems

The functionality of many modern advanced computer systems -- such as, e.g., wireless sensor networks, the Internet and other kinds of networks, and control systems -- is crucially dependent on the amount of time that passes during/between events. Furthe rmore, such advanced and often critical systems must be well understood before deployment. The design of these systems should therefore be modeled and thoroughly analyzed at an early (and at different stages) in the system development process. Advanced real-time systems pose a challenge to modeling tools in that different aspects, such as, e.g., real-time and probabilistic behavior, object orientation, communication, data types, etc., must be captured, and in that they should provide not only simulatio n or verification capabilities, but preferably a wide range of analysis techniques (including the before-mentioned two extremes). Ølveczky and Meseguer have developed a formal language and tool, Real-Time Maude, that provides a flexible and general mode ling language that can naturally model many aspects of a real-time system at different levels of abstraction. The tool provides a spectrum of time-specific analysis commands, including simulation/prototyping and different kinds of exhaustive state space exploration. Real-Time Maude has been applied to a range of advanced applications, including sophisticated multicast protocols for active networks and the Internet, new state-of-the-art scheduling algorithms, and new wireless sensor network and scheduli ng algorithms, that are beyond the range of systems that can be specified by popular automaton-based formalisms. Indeed, we believe that our work on the OGDC wireless sensor network algorithm represents the first formal modeling and analysis of advanc ed wireless sensor network algorithms. In this project we aim at extending Real-Time Maude's capabilities and at applying the tool on advanced systems. In particular, to make analysis feasible for large and advanc