Rodolfo Gomez

Research Associate

Photo of RS Gomez, if available
  • Room SW16
    School of Computing
    University of Kent,     CT2 7NF

Publications

My publications are available from the Computer Science department publications repository.

Research Interests

I belong to the following research groups:

Keywords: Formal Methods, Concurrency Theory, Real-time Systems.

I am interested in concurrency theory and practical applications of formal methods, in particular the application of formal methods to the specification and verification of real-time systems.

Broadly speaking, a real-time system is one whose correct behaviour depends on time constraints, e.g., communication protocols, air-traffic and rocket guidance systems (see also what Wikipedia has to say about real-time systems). The complexity of real-time systems is such that specifications are prone to contain subtle errors, which are hard to find. Moreover, in safety-critical applications, ensuring that real-time systems behave as expected is crucial to avoid possible loss of human lives. Hence the importance of using formal methods in the design and analysis of real-time systems, which offer rigorous mathematical analysis and therefore provide confidence in the development process.

My ongoing research considers temporal logics (including Interval Temporal Logic) and timed automata theories. In particular, I study the problem of timelocks in formal verification of real-time systems. Timelocks are states where the time cannot diverge; timelocks are counterintuitive (systems cannot prevent time from passing!) and affect the verification of correctness properties (timelocks may hide errors in the design that will still arise in the implementation). Formal notations cannot (in general) prevent the occurrence of timelocks in specifications because (semantically) ''stopping time progress'' is necessary to model urgency (this is used to distinguish events that may happen from those that must happen in a certain time interval).

See our book on concurrency theory:

Concurrency theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems

Howard Bowman and Rodolfo Gomez

Springer, 2006

EPSRC Postdoctoral Fellowship on Theoretical Computer Science: "Addressing Current Limitations of Real-time Model-checking"

The general objective of this project is to improve the available tool support for the verification of real-time systems. To this purpose we consider two lines of research.

The first line of research aims to complement the facilities offered by Uppaal to detect timelocks and Zeno runs. This can be done efficiently by exploiting the structure of cycles and synchronisation in the automata networks. The ZenoChecker tool (see below) is one of our first results.

A second line of research aims to extend Uppaal's requirements language with an ITL chop-like sequential composition operator. The challenge is to investigate to what extent this can be accomplished via test automata, without disturbing Uppaal's efficient algorithms.

More details can be found at the project's webpage .

Some tools I have developed:

pitl2mona : This is a tool to translate PITL formulae to MONA programs. PITL is a rich propositional subset of Moszkowski's Interval Temporal Logic. MONA is an efficient BDD-based, automata-theoretic decision procedure for WS1S, a logic with the expressive power of regular languages and (consequently) a worse-case non-elementary decision procedure. Both PITL and WS1S have the same expressive power and complexity. Using PITL2MONA as a front-end, we use MONA as a decision procedure for PITL that is able to cope with the inherent complexity.

ZC : This is a tool to check absence of Zeno runs (non-divergent, infinite runs) in Uppaal networks. This tool exploits the structure of cycles and synchronisation in the networks to quickly discover Zeno runs, highlighting all the possible sources.

TAD2TA : This is a tool to translate Timed Automata with Deadlines to Uppaal Timed Automata networks.

LIDLmd2TA : This is a tool to generate synchronous observers from LIDLmd formulae, and link them to Uppaal networks. This allows for the verification of complex properties that cannot be expressed in Uppaal's requirements language.