A larger research effort is on the definition of a modal logic to reason on global applications. Models for the logic are space-time diagrams describing the behaviour of a set of components that communicate asynchronously. The contribution is that it is possible to reason about properties that involve several components, even in the absence of a global clock. The motivation for this work is that the existing logics for distributed systems do not have the right expressive power to reason on the systems behaviour, when the communication is based on asynchronous message passing. On the other side, asynchronous communication is the most used abstraction when modelling global applications.
The main activities on requirements engineering include definition of methods and techniques for the extraction of semantic information from natural language requirements. A prototype environment has been realized and is on the course of being revised and completed with support for generation of initial ground models to be further transformed by the specifier. Other research is concerned with the structural analysis of requirements documents, the integration of industrial standard representation (like UML), and quantitative analysis of requirements processes supported by the environment. Part of these activities have been conducted in collaboration with European partners inside the ESPRIT Network of Excellence RENOIR and the MURST co-funded Project AI*IA, and thanks to an IBM Eclipse Innovation Award.
One thread of activity continues the research line of high-level modeling and analysis of systems (control software, instruction set architectures, programming languages implementations, and hardware design languages). Practical and concrete experience was gained during the last years in four main projects. The first of them is the FALKO project on the high-level specification and implementation of a train simulation and planning system (Siemens Corporate Research, 1997-1999). The second one is the Java/JVM project (realized in cooperation with researchers at the University of Ulm, at ETH Zürich and at Siemens Corporate Research, 1998-2001) on a validated and verified specification and implementation of Java and the JVM architecture. The third is the ASM-UML project (in cooperation with University of Bergamo and Milan/Crema (Italy), Karlsruhe/D and Oxford/GB) to provide a rigorous and complete semantics to central UML concepts which allow one to link in a controllable way UML and ASM design methods. The fourth is the R2D2 project, in collaboration with Microsoft Research (Cambridge/UK lab), to study the control software of robots designed to live together with people. On the basis of this experience the following five projects are being carried out: a) the ASM project where the focus is on the development of practically useful design and analysis methods and tools, in particular focused on refinement and executability of ASM specifications, b) the C#/CLR project (in cooperation with ETH Zürich) on ASM reuse for a validated and possibly verified specification of C# and of its underlying virtual machine CLR, c) the requirements engineering environment is being extended to generate high-level ASM models and initial UML models from the same requirements base, so that the two are linked by construction, d) the web service interaction pattern project (in collaboration with SAP Research/D and Queensland University of Technology/Australia), e) Self-evolving programs project (in collaboration with Microsoft Research, Cambridge/UK) on software capable of changing its structure to adapt to the executing environment.