Research Interests
My research interests include software engineering and theoretical computer science, with particular reference to the following:
1. The specification, validation and verification of safety-critical and real-time systems.
2. Theory and applications of automata and formal languages
Specification, validation and verification of safety-critical and real-time systems
The goal of my research has been to provide language support to the formal specification of real-time and safety-critical systems, and to design an environment which provides tools for writing and analyzing formal specifications, and thus assess their validity before any development takes place. In particular, such an environment should support the execution of formal specifications. By executing formal specifications and observing the behavior of the specified system, one can check whether specifications capture the intended functional requirements or not. In the description of large and complex systems, however, one often needs to structure the specification into modular, independent, and reusable parts. In such a case, beyond formality, executability, rigor, and absence of ambiguity, other language features become important, such as the ability to structure the specifications into modules, to define naming scopes, to produce specifications by an incremental, top-down process, to attribute a separate level of formality and detail to each portion of the specification.
The outcome of this work has been a new language, called TRIO+, which is an object-oriented version of metric temporal logic, with a graphical notation. The language has been applied to various real life case studies. A complete environment has been built for the language, including a graphical, syntax-driven editor, a syntax checker, an interpreter, a test case generator. Test case generation starting from modular specifications has been introduced and various supporting tools have been developed. Many applications in various domains (such as railways and power generation) have been developed in cooperation with various industries.
Theory and applications of automata and formal languages
In the past year, various families of rewriting systems have been introduced and studied in literaturee in order to extend the power of context-free grammars. The motivation came from fields as diverse as compiler design and computational linguistics, since both the syntax of programming languages and the syntax of natural languages have context-sensitive features. However, context-sensitive grammars, while powerful enough, are PSPACE-complete. The interest has been in grammar formalisms that do no sacrifice the attractive features of context-free languages, such as polynomial-time parsing and various other closure and decidability properties. The outcome of the research at has been the study of a new class of automata and grammars, extending push down automata and context free grammars, and the development of parsing algorithms for this class. Also, various interesting properties of the formalism have been proved, showing also the mathematical relationships with other formalism introduced by various authors. Recently, another line of research has considered a new formalism, called Associative Language Description, based on local testability concepts, that eliminate from the Context-Free model those languages (such as counting languages) which are not useful in practice.
An application of automata and compiler theory is currently being developed in an Esprit project, in cooperation with the Université de Marne-la-Valleé, in order to specify, verify and execute Graphic User Interfaces.