prof.dr.ir. A. Rensink (Arend)

FormaSig

Formal Methods in Railway Signalling Infrastructure Standardisation Processes

European railroad infrastructure managers have joined forces in the EULYNX organisation with the aim to arrive at standardised interfaces between interlockings and trackside equipment. Standardisation efforts will significantly reduce the cost of ownership of signalling systems. Indeed, if the interfaces and architecture of a signalling systemare standardised, then different components can be procured from different suppliers, thereby enabling competition and preventing vendor lock-in situations. Furthermore, approval processes can be harmonised and simplified, and will thus become more efficient. The goal of the FormaSig project is to formally verify these interfaces, and check compliance with the standard, so that delivered products satisfy certain properties. Using the formal model, it can also be more thoroughly tested whether a delivered component complies with the standard (formal model-based testing). Furthermore, the application of formal verification techniques will help to validate to what extent the standard guarantees national requirements and they will help to improve tender documents. We could, e.g., also make a formal model of the national requirements and then conduct a thorough mathematical comparison with the formal model of the standard, and test cases derived from the formal model of the standard could be included in tender documents.

Aselsan - University of Twente cooperation

This is a cooperation framework between the University of Twente and Aselsan, Ankara, Turkey. The framework actually consists of a set of individual projects, which are carried out concurrently and cooperatively, each by a Master - PhD student or a PhD student.

EACSC

Effective Alignment in Computer Science Curricula

Alignment in teaching refers to the triangle of content, teaching and testing modes: they should fit together. You cannot effectively teach Defense Against the Dark Arts without a wand, or test it effectively through a multiple choice form. Neither does it seem sensible to test programming skills through a hand-written test; yet that is often still what happens in Computer Science. Lasting innovation is hampered by practical obstacles such as maintainability and scalability of the chosen forms. It occurs on the side of the students (in a programme with 200 students, extensive individual feedback may be infeasible) but also on the side of the teachers (a form that works due to the enthusiasm of its inventor may no longer be effective when that spark has died down or the course is taken over by a colleague). On the whole, we can characterise Computer Science students on the one hand by a large degree of technical creativity and a drive to understand and control the working of (electronic) devices, and on the other hand by an inward rather than outward focus. These characteristics should be taken into account in the choice of teaching and testing methods in a Computer Science curriculum.

GROOVE

Graphs for Object-Oriented Verification

The aim of this project is to develop and implement model checking techniques for object-oriented designs and programs, based on a representation of program states as graphs and computation steps as graph transformations. The advantage of this representation over the more traditional one (which is essentially based on fixed state vectors determined at compile time) is that the graph formalism quite naturally captures the dynamic nature of object-oriented systems that is due to object (de)allocation and patterns of method invocations. Furthermore, graphs offer new insights in state abstraction, one of the most promising principles to combat state space explosion. Finally, the representation of objects as graphs provides a direct link to popular design notations such as those offered by the UML, and the use of graph transformation is currently advocated in several earlier stages of software development; thus, there is a realistic hope of integrating graph-based object-oriented verification techniques into a more encompassing, truly useful software engineering process.

CHARTER

Critical and High Assurance Requirements Transformed through Engineering Rigour

CHARTER is developing concepts, methods, and tools for embedded system design and deployment that will enable developers to master the complexity and substantially improve the development, verification and certification of critical embedded systems.

TREsPASS

Technology-supported Risk Estimation by Predictive Assessment of Socio-technical Security

By integrating European expertise on socio-technical security into a widely applicable and standardised framework, TREsPASS will reduce security incidents in Europe, and allow organisations and their customers to make informed decisions about security investments. This increased resilience of European businesses both large and small is vital to safeguarding the social and economic prospects of Europe.

ATOMYSTE

ATOm splitting in eMbedded sYStems TEsting

The Atomyste-project aims at developing methods and tools to cope with the problem of atom splitting (or action refinement) in automatic, formal conformance testing of embedded, reactive software systems. Atom splitting involves the change in granularity of test primitives from test derivation to test implementation. This change has semantic consequences which are currently not well-understood, but which may have severe implications for the validity and soundness of the derived tests. The starting points for Atomyste are the theories of action refinement and of conformance testing. The purpose is to combine these theories in such a way that semantically sound and practically usable methods and tools can be developed to support atom splitting in testing.

AOSD-Europe

Network of Excellence on Aspect-Oriented Software Development

AOSD-Europe will harmonise and integrate the research, training and dissemination activities of its members in order to address fragmentation of AOSD activities in Europe and strengthen innovation in areas such as aspect-oriented analysis and design, formal methods, languages and applications of AOSD techniques in ambient computing. Through this harmonisation, integration and development of essential competencies, the AOSD-Europe network of excellence aims to establish a premier virtual European research centre on AOSD

GRASLAND

Graphs for Software Language Definition

The purpose of this project is to define a meta-language in which all aspects of Software Languages (SLs), besides their concrete syntax, can be defined in a consistent manner. As a common formal foundation of this metalanguage we propose graphs and graph transformations, which we believe to be powerful enough to capture all relevant SL aspects. This meta-language will enable us to provide semantic definitions of the source and target SLs involved in a given model transformation on a compatible basis; this in turn will enable us to precisely formulate and check the requirement of correctness preservation. We believe these abilities to be essential in realizing the full potential of MDA.