Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Jan Peleska > Deutsch
English
 

Projects
 

Projects in Jan Peleska's Research Team

CPOT-SM - Complete Property-oriented Testing with Symbolic Methods (2019-10-01 - 2022-09-30)

CPOT-SM is a project funded by the DFG. Its research focus is on complete property-oriented and model-based testing. The detailed project description can be found on the CPOT-SM home page.

ITTCPS - Implementable Testing Theories for Cyber-physical Systems (2015-2017)

ITTCPS is a so-called M4 exploratory project funded by the University of Bremen in the context of the German Universities Excellence Initiative.

The objective of this project is to elaborate a novel view on concurrent systems semantics and apply this to the fields of model-based testing and model checking for cyber-physical systems (CPS).

The "classical" semantic approaches available today do no longer cover all phenomena observable in modern hardware architectures and in highly distributed CPS networks with many participants. The latter demand adequate behavioural models reflecting dynamicity of system configurations, evolution of behavioural assertions, large numbers of replicated components, and mixed discrete and time-continuous behaviour. The main challenge, however, consists in inventing a practicable method for translating theories elaborated in one semantic framework into a corresponding theory of another.

The unique selling points of this project do not only consist in the basic research contributions to the field of semantic frameworks, but in a very practical implication: advanced model-based testing tools and model checkers operate on suitable encodings of a given system model's behavioural semantics. To apply a test strategy or to prove the validity of a model property, these tools use theories established in a specific semantic framework. The current state of the art only allows to apply these theories to concrete system models interpreted in the same framework. Mappings to other frameworks are extremely complicated and cumbersome to verify. With the novel method of semantic navigation to be elaborated in this project, easy - even automated - mappings of existing theories established in one semantic framework into others will become possible. This enables an effective application of methods and tools to modelling formalisms originally interpreted in other semantic frameworks.

More details can be found on the ITTCPS homepage.

STEVE - System-Technik und Virtuelle Erprobung

This project is founded by the german BMWI (Bundesministerium für Wirtschaft und Energie) within the LuFo V-1 (Luftfahrtforschungsprogramm V, part 1). The University of Bremen participates in work package 220 of the STEVE project which is focused on Virtual Integration Platforms Next Generation (VIP-NG). This workpackage aims to define a common way for test bench components to interact with each other so that a disctributed test bench can be defined that contains constituents from different suppliers. These constituents must work together, can be centrally configured and controlled to provide the test bench functionality. For this, a communication layer is defined that is used by all constituents to communicate with each other. Within work package 220, University Bremen leads the sub-work package WP222 that defined the communication layer between the constituents.

The project is lead by Airbus Germany and cooperates with a partner project DGAC lead by Airbus France. A new term and project called Virtual Hybrid Testing Next Generation (VHTNG) has been defined by Airbus (France and Germany) that is used instead of the term VIP-NG, as well.

COMPASS - Comprehensive Modelling for Advanced Systems of Systems (2011-2014)

The COMPASS consortium is a group of researchers and companies committed to collaborative research on model-based techniques for developing and maintaining Systems of Systems (SoS).

Modern networking technologies let systems cooperate by sharing resources and offering services to one another so that the resulting system of systems has a behaviour that is greater than just the sum of its parts. Although there are great opportunities here, the design of innovative products and services that take advantage of Systems of Systems (SoS) technology is hampered by the complexity caused by the heterogeneity and independence of the constituent systems, and the difficulty of communication between their diverse stakeholders. Developers lack models and tools to help make trade-off decisions during design and evolution leading to sub-optimal design and rework during integration and in service. The work in COMPASS is inspired by the vision that complex SoSs can be successfully and cost-effectively engineered using methods and tools that promote the construction and early analysis of models.

The COMPASS research agenda involves:

  • Developing a modelling framework for SoS architectures.
  • Providing a sound, formal semantic foundation to support analysis of global SoS properties.
  • Building an open, extendible tools platform with integrated prototype plug-ins for model construction, simulation, test automation, static analysis by model-checking, and proof, and links to an established architectural modelling language.
  • Evaluating technical practice and advanced methods through substantial case studies.

For additional information see COMPASS

TCGen: Test Case Generator and Error Diagnostics (2007 - 2008)

The TCGen project is carried out in co-operation with Verified Systems International GmbH, funded by BIG Bremer Investitions-Gesellschaft mbH (research grant 2INNO1015B).

The goal of this project is to combine two closely related technological novelties and integrate them into the test tool RT-Tester:

  • Model-based test case generation: Facilitates the automatic derivation of the required test cases and associated test data from software specifications as generated with commonly used CASE tools (requirements tests), as well as from the source code to be tested (code coverage tests).
  • Automated support for error diagnostics: Methods which help the test experts to find faults in the source code which caused the errors observed during testing.

Methods for model-based test case generation have been pursued by different research groups and tool vendors for nearly a decade. But only the progress that was achieved in different research fields of computer science and mathematics during the last two years facilitate an implementation demonstratably fit for industrial use.

The recently discovered relation between test case generation and error diagnostics methods led to further investigation: Algorithms used for generation of test data in particular test situations can also be used to determine the potential impact of a software component to an observed error.

For additional information see http://www.informatik.uni-bremen.de/agbs/projects/tcgen/index_e.html

E-CAB: E-enabled Cabin and Associated Logistics for Improved Passenger Services and Operational Efficiency (2006-2009)

E-Cab is an Integrated Projected eligible for funding under the 3rd Aeronautics Call 3A of the 6th Framework Programme listed under selected subject number 2 - Integrated approach to an e-enabled cabin and associated logistics for improved passenger services and operational efficiency. As such it responds primarily to the objectives of the Thematic Priority 1.4 Aeronautics and Space, Work Programme 2002-2006, but also to a wider set of objectives set out in the Strategic Research Agenda 2nd edition (SRA2) issued by the Advisory Council for Aeronautics Research in Europe (ACARE).

The successful completion of this project shall provide the airports and airlines with an environment that enables the possibility of offering a step change in service concepts, ensuring enhanced passenger convenience and increased competitive advantage for the European participants.

Participants of E-Cab :

  • Aircraft Manufacturers: Airbus Deutschland GmbH, DASSAULT AVIATION

  • Large Industrial Companies: Ascom (Switzerland) Ltd., Diehl Aerospace GmbH, EADS Deutschland GmbH, GIUNTI Labs S.r.l., Rheinmetall Defence Electronics GmbH, SELEX COMMUNICATIONS, Siemens IT Solutions and Services GmbH & Co. OHG, SITA-SC, Terma A/S, THALES AVIONICS UK, THALES AVIONICS SA, Ultra Electronics AIRPORT SYSTEMS

  • Small and Medium Enterprises: B&W Engineering GmbH & Co. KG, Bucher Leichtbau AG, CeBeNetwork France S.A.R.L, Dansk Teknologi Udviklingsaktieselskab, IDENTEC SOLUTIONS AG, Jettainer GmbH, Microtech International Ltd., OnAir N.V., TriaGnoSys GmbH

  • Research Centers: CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE, Centro IBERLog, FUNDACIÓ ROBOTIKER, Nederlands Organisatie voor toegepastnatuurwetenschappelijk onderzoek

  • Universities: Cranfield University, University of Malta, Center of Information Technology (TZI) - University of Bremen

For additional information see http://www.informatik.uni-bremen.de/agbs/projects/ecab/index_e.html

KATO: Innovative Cabin-Technology (2004-2007)

The research project KATO - in collaboration with Airbus Deutschland GmbH - is located within the German aerospace research programme LUFO III.

KATOs main objective is the development of new methods, tools and technologies to improve the development and the verification of future aircrafts by providing means for fault avoidance, early fault detection and fault diagnosis. Thus, the aim of KATO is to reduce costs and time for development and verification significantly.

For additional information see http://www.informatik.uni-bremen.de/agbs/projects/kato/index_e.html

HYBRIS: Efficient Analysis of Hybrid Systems (1999 - 2005)

This project is a sub-project in the DFG-funded collaboration Integration of Software Specification Techniques for Scientific Engineering Applications . The project integrates description techniques widely used in the engineering sciences (timing diagrams and differential equations) with formal specification techniques that have been mostly used in the computer science communities (Timed CSP and Duration Calculus). The integrated application of these techniques is demonstrated by means of case studies from the field of railway control systems. Furthermore, it will be investigated whether concepts based on partial-order theories can be applied in the context of these specification techniques. For additional information see http://www.informatik.uni-bremen.de/agbs/projects/hybris/index_e.html

VICTORIA: EUROPE MOBILIZES TO DESIGN A NEW GENERATION OF COMMERCIAL AIRCRAFT ELECTRONIC SYSTEM (2001 - 2004)

The VICTORIA Project will be launched on January 9th-10th, 2001 in Toulouse, at ENSICA (Ecole Nationale Supérieure d'Ingénieurs de Constructions Aéronautiques) under the leadership of Thales Avionics, formerly Thomson-CSF Sextant. Attending will be representatives of the 32 other participants, as well as the European Commission.

This project brings together 33 industrial companies, R&D centres and universities from Europe's Aerospace community (see list below). The objective is to design, prepare and validate a new architecture and a new system that integrates all on-board functions for commercial airliners.

During the recent years, the needs for electronics on-board long and medium range airliners have grown very significantly. Given the increasingly congested conditions at airports, airline crews require navigation, control and communication resources that are both more deeply integrated and technologically sophisticated. On the other side, to save time and improve the comfort of their customers, airlines are seeking to enhance the in-flight services available to passengers by implementing computer-based solutions at every level. This also encompasses flight and passenger management system, which falls within the scope of the Onboard Information System or OIS. Finally, there is a pressing need for sophisticated In-Flight Entertainment systems, including on demand video, Web access and email, with screens available at every seat.

Despite the emergence of those needs, the European industrial companies could not individually address them so far. But the recent evolutions in electronics and communication technologies make it now possible to respond successfully to them.

What's more, the engineering design specialists at aircraft manufacturers and equipment suppliers have clearly identified the efficiency and economic viability of Integrated Modular Electronics (IME). This concept aims to standardise the interfaces between basic resources (computers and operating systems) and onboard applications. This will open up the market and support ongoing development and enhancements in both areas. The main beneficiary of these improvements will be the passengers, who will enjoy an enhanced and more economical flight experience. At the industrial level, deployment of an architecture such as this will lead to far-reaching changes in the work done by suppliers, accompanied by a complete restructuring of the subcontracting system.

The Victoria project, which builds on the work accomplished by the Nevada and Pamela projects, also part of the European R&D Framework Programmes, constitutes one cornerstone of this initiative. Thales Avionics will coordinate this major three-year project. Alongside its European partners, Thales is committed to meeting the challenges of developing new technologies in order to respond to market demand and consolidate its leadership in Europe.

Participants of VICTORIA :

  • Aircraft manufacturers: Aerospatiale Matra Airbus (EADS Airbus SA), EADS Airbus GmbH, BAE Systems Airbus, Alenia Aerospace

  • Helicopter manufacturers: Eurocopter, GKN/Westland

  • Systems and equipment suppliers: THALES Avionics, SMITHS Group, Diehl Avionik Systeme, Ultra, Comsys, Skysoft, Bae Systems Avionics, Liebherr, VDO-L, AOA, Nordmicro, Fokker Elmo, Ericsson Saab Avionics, Intertechnique, SAGEM, AIM, SINTERS, TERMA, KID, MESSIER BUGATTI

  • R&D Centres: NLR (Pays-Bas), DERA (GB) , ONERA (F)

  • University research laboratories: Universities of York, Bremen, Darmstadt, PEI/NMRC (attached to the university of Cork ), ICCS (Institute of Communication and Computer System) of Athens university.

Graphical Methods and Tools for Test Specification (1999 - 2003)

This is a research project funded by the ISP Bremen. The project objective is to develop a graphical non-standard simulation method and tool for the creation of formal Timed CSP test specifications. Typically, this method is used in the context of automated testing of embedded real-time systems with complex user interfaces (our first industrial application is the hardware-in-the-loop test of the Airbus Cabin Intercommunication Data System CIDS described below). While the problem of generating, executing and evaluating test executions from Timed CSP specifications is already solved and supported by appropriate tools, the creation of the formal specifications still represents a serious stepping stone, since it does not only require expertise about the application to be tested but also considerable skill in the field of Formal Methods. Our graphical test specification method aims at facilitating this task. The method is based on two types of graphical models: (1) A virtual reality representation of the system interface and its operational environment and (2) a graphical meta language allowing to control the test specification process with respect to reuse and combination of of components, definition of generic parameters, quantification and abstraction of interface details. We use the term `non-standard simulation', because in our context simulation is not performed to animate an existing model of system behaviour. Instead we start with an incomplete model containing only basic interface specifications and create a model which is sufficiently complete for testing purposes by means of user interactions in the simulation environment.
  • J. Peleska, S. Bisanz and I. Fiss:
    Non-Standard Graphical Simulation Techniques for Test Specification Development. Submitted to ESM '99 (1999).

AIRBUS-ASTS: Automatic Hardware-in-the-Loop Test System for Daimler-Chrysler Aerospace Airbus (1998 - )

This is an industrial project with a collaboration between Daimler-Chrysler Aerospace Airbus, KID-Systeme (Hamburg/Buxtehude), Verified Systems International GmbH (Bremen) and the Bremen Institute of Safe Systems BISS , department of the Center for Computing Technology TZI . The project objective is to develop a hardware-in-the-loop test system for automated tests of the Cabin Intercommunication Data System CIDS which has been developed by KID-Systeme for the Airbus family. The test system (called ASTS ) consists of a computer network directly interfacing to the CIDS embedded computer, stimulating the CIDS input interfaces and monitoring its output sequences. Test executions are generated from and checked on-the-fly in real-time against Timed CSP specifications. For this purpose, the VVT-RT test software developed by Verified Systems International GmbH in collaboration with the BISS has been integrated on the ASTS hardware. For (preliminary) additional information see For the underlying testing theory see
  • J. Peleska:
    Testing Reactive Real-Time Systems. Tutorial, held at the FTRTFT '98. Danmark Technical University, Lyngby (1998).
  • J. Peleska and M. Siegel:
    From Testing Theory to Test Driver Implementation. In M.-C. Gaudel and J. Woodcock (Eds.): FME '96: Industrial Benefit and Advances in Formal Methods. LNCS 1051, Springer-Verlag, Berlin Heidelberg New York (1996) 538-556.
  • J. Peleska and M. Siegel:
    Test Automation of Safety-Critical Reactive Systems.
    South African Computer Jounal (1997) 19: 53-77.
    Also available as Bericht Nr. 9614, Dezember 1996, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel (1996). compressed postcript file (121KB)
  • J. Peleska:
    Formal Methods and the Development of Dependable Systems.
    Habilitationsschrift, Bericht Nr. 9612, Dezember 1996, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel (1997). compressed postcript file (519KB)

FTC-TEST: Hardware-in-the-Loop Test for the Daimler-Chrysler Aerospace DMS-R Fault-Tolerant Computer (1997 - 1998)

This is an industrial project with a collaboration between Daimler-Chrysler Aerospace RI (Bremen), Verified Systems International GmbH (Bremen) and the Bremen Institute of Safe Systems BISS , department of the Center for Computing Technology TZI . The project objective was to perform a hardware-in-the-loop test for the FTC fault-tolerant computer developed by Daimler-Chrysler Aerospace RI for the Data Management System DMS-R in the International Space Station ISS . As in the AIRBUS-ASTS system, tests are performed using the VVT-RT test automation system in a distributed test system handling specialised FTC interfaces. For detailed information see the references given for the FTC-VERIFICATION project.

FTC-VERIFICATION: Verification Suite for the Daimler-Chrysler Aerospace DMS-R Fault-Tolerant Computer (1995 - 1998)

This is an industrial project with a collaboration between Daimler-Chrysler Aerospace RI (Bremen) and the Bremen Institute of Safe Systems BISS , department of the Center for Computing Technology TZI . The project objective was to perform a verification suite for the software layers implementing the avionics interface (MIL-STD 1553 bus) and the fault management layer. The software consists of about 25,000 lines of OCCAM code. The verification objectives were to investigate
  • deadlock freedom,

  • livelock freedom,

  • critical perfomance bottle necks,

  • correctness of the Byzantine protocol implementation used in the fault management layer.

The investigation of bottle necks was performed using an abstraction of the OCCAM code to Stochastic Petri Nets, the other properties were performed using suitable abstractions from OCCAM to CSP. The CSP abstractions were analysed by model checking for local properties which were combined using compositional reasoning and generic theories. For additional information see

FSDT-TEST: Automatic Hardware-in-the-Loop Test for South African Railways (1997 - 1998)

This is an industrial project with a collaboration between Tansnet (South African Railways), the University of Cape Town and the Bremen Institute of Safe Systems BISS , department of the Center for Computing Technology TZI . The project objective was to perform an automated hardware-in-the-loop test for the FSDT Fail Safe Data Transceiver which is used for the communication of safety-critical information between interlocking systems.

ABRIXAS-TEST: Automatic Hardware-in-the-Loop Test for OHB (1997 - 1998)

This is an industrial project with a collaboration between OHB (Bremen) and the Bremen Institute of Safe Systems BISS , department of the Center for Computing Technology TZI . The project objective was to perform an automated hardware-in-the-loop test for the PTC Power and Thermal Controller of the ABRIXAS research satellite developed by OHB. A special feature was that the PTC is a hybrid system: The tests had to stimulate and monitor both discrete and time-continuous system interfaces.

UNIFORM: Uniform Workbench for Formal Program Development Tools (1995 - 1998)

This is a project funded by the German BMBF; the project partners are Bremen University, Oldenburg University and Elpro LET GmbH Berlin. The UniForM Workbench is a generic framework, instantiated with specific tools for methods to handle communicating distributed systems and real-time requirements. The combination of methods in a logically consistent way and the development of correct transformation tools, a basic aspect of quality assurance, are demonstrated. The industrial potential of the UniForM Workbench is illustrated by a case study from industry, the development of a decentralized control unit for single-track tramway networks. For additional information see http://www.informatik.uni-bremen.de/~uniform

TCCC-TEST: Automatic Hardware-in-the-Loop Test for ELPRO (1994 - 1995)

This project was performed by Jan Peleska for ELPRO LET GmbH, while working as a consultant in the field of quality assurance, verification, validation and test for companies producing embedded controllers. The objective was to design test cases and check test executions for the Tramway Crossing Control Computer TCCC developed by ELPRO LET GmbH. This task was performed using the first version of the VVT-RT test automation system which was developed by Jan Peleska. For additional information see
  • J. Peleska:
    Test Automation for Safety-Critical Systems: Industrial Application and Future Developments. In M.-C. Gaudel and J. Woodcock (Eds.): FME '96: Industrial Benefit and Advances in Formal Methods. LNCS 1051, Springer-Verlag, Berlin Heidelberg New York (1996) 39-59.

BRR-STF: Hardware-in-the-Loop System Test Facility for BMW Rollce-Royce (1993 - 1995)

This project was performed by DST Deutsche System-Technik GmbH (Kiel) for BMW Rollce-Royce with Jan Peleska as DST project leader. The objective was to develop a computer network (the System Test Facility STF) interfacing to the BRR 700 aircraft engine controller to perform hardware-in-the-loop tests by means of a script language allowing to specify sequences of interface manipulations and evaluation conditions.

AIRBUS-CIDS: Development of Application and System Software for the AIRBUS CIDS System (1990 - 1993)

This project was performed by DST Deutsche System-Technik GmbH (Kiel) for Daimler-Benz Aerospace Airbus, KID-Systeme with Jan Peleska as DST project leader. The task was to develop, test and verify software for the Airbus A330/340 cabin communication system CIDS. In this project, considerable quality improvements were gained by using formal specification techniques. For additional information see

PHILIPS-DCP: Development of a Fault-Tolerant Dual Computer System (1985 - 1989)

This project was performed by Philips Systeme und Sondertechnik (Kiel) with Jan Peleska as development team leader. The project objective was to develop a fault-tolerant dual computer system using dynamic redundancy concepts to exploit the additional computing power of the standby computer while both computers were in normal operation mode. Formal methods were used to specify and verify the fault management software layer implemented in the dual computer system. For additional information see
  • J. Peleska:
    Formal Methods and the Development of Dependable Systems.
    Habilitationsschrift, Bericht Nr. 9612, Dezember 1996, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel (1997). compressed poscript file (519KB)
  • J. Peleska:
    Design and verification of fault tolerant systems with CSP.
    Distributed Computing (1991) 5: 95-106.
  • J. Peleska:
    Formale Methoden beim Entwurf ausfallsicherer, verteilter Systeme.
    In Lippold, Schmitz (Eds.): Sicherheit in netzgestuetzten Informationssystemen. Proceedings des BIFOA-Kongresses SECUNET '92, Vieweg (1992) 293-308.
  • J. Peleska:
    CSP, Formal Software-Engineering and the Development of Fault-Tolerant Systems. In Vytopil (Ed.): Formal Techniques in Real-Time and Fault-Tolerant Systems. Kluwer Academic Publishers (1993) 167-207.

Jan Peleska, last update 01-FEB-1999
 
   
Author: Elmar Prüße 		 
  AG BS 
Last updated: November 2, 2022   Impressum