You are here: DASMOD > Projects > VerSiS


Start of topic | Skip to actions

VerSiS: Verification and Simulation of Embedded Hybrid Systems

Project Topic

The purpose of the VerSiS Project is to add formal verification to the design process of reliable embedded systems.

Project Description

Formal verification is crucial in the design process of reliable embedded systems. The particular challenge is due to the heterogeneity of the involved technical systems. Despite of custom digital hard- and software components, also actuator and sensor componets play an important role as interfaces to the environment. The development of new design and verification methods with integrated work flow is the main subject of this project.

The close cooperation of the involved working groups, whose main competences reflect various aspects of hybrid embedded systems, is the essential condition for putting into practice this reasearch project. The approaches developed by the Reactive Systems Group will be extented for describing analog systems, which obey differential equations.

Starting with these hybrid programs a description for simulation, verification and generation of hard- and software will be obtained. For verification of digital subsystems computational methods by the Algebra, Geometry and Computer Algebra Group will be used, which reduce Boolean problems to equivalent problems in polynomial rings.

Sensor and actuator components will be verfied using methods developed by the Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems). In particular efficient symbolic methods should be applied for verification of tolerance-affected components, together with new interval arithmetical approachs on the one hand, and modern modelling techniques for multi-physical systems on the other.

Finally, the developed methods should be evaluated with respect to case scenarios from the area of robotics, which will be provided by examples of the behaviour based control of the Robotics Laboratory.

Project Members

Project Chair

Participating Research Groups

  • Algebra, Geometry and Computer Algebra Group (Department of Mathematics)
  • Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) (Fraunhofer Institute for Industrial Mathematics (ITWM))
  • Reactive Systems Group (Department of Computer Science)
  • Robotics Laboratory (Department of Computer Science)

Scientific Personnel

Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) (Fraunhofer Institute for Industrial Mathematics (ITWM))
  • Dr. Alexander Dreyer
  • Dr. Jochen Broz

Reactive Systems Group (Department of Computer Science)
  • Dr. Raffaella Gentilini

Robotics Laboratory (Department of Computer Science)
  • Martin Proetzsch

Algebra, Geometry and Computer Algebra Group (Department of Mathematics)
  • Dipl.-Math. Oliver Wienand

External Cooperation

Mathematisches Forschungsinstitut Oberwolfach
  • Michael Brickenstein

Electronic Design Automation Group (Department of Electrical Engineering and Information Technology)
  • Dr.-Ing. Markus Wedler
  • Evgeny Pavlenko

Project KryFoVe
  • M.Sc. Stanislav Bulygin

Project Events and Achievements

Project start: 01.10.2005 with a preliminary duration until the end of 2007

Project Dates

Early 2006: Initial consultations and agendae.

March 15/22, 2006: Internal Workshops including presentations of the involved research groups and the state of the art of corresponding research areas.

March 31 and April 10/11, 2006: Initial meetings for preparation of a joint implementation by members of Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group, and Mathematisches Forschungsinstitut Oberwolfach for initializing the Gröbner-basis approach for solving verification problems of digital circuits on bit-level.

April 28, 2006: Internal Workshop including discussion about ongoing activities and recent work. Briefly, Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) proposes to model the whole combined digital/analog system path of a suitable robot of Robotics Laboratory. The model can then be reduced using model reduction techniques, which simplifies formal verification of the system. Also, synergies between Reactive Systems Group and Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) may result from combining hybrid automata and interval-methods. Furthermore, Reactive Systems Group has started formal verification of critical subsystems of an outdoor robot of Robotics Laboratory.

May 4/5, 2006: Tutorial workshop concerning the computer algebra tool SINGULAR, developed by Algebra, Geometry and Computer Algebra Group, and the reactive systems verification tool AVEREST, developed by Reactive Systems Group. Planning of an interface between the two tools for dealing with the analysis of reactive systems within the computer algebra framework of SINGULAR. In addition consultation of Dr. Alexander Dreyer (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems)) and Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) together with the SINGULAR team of the Algebra, Geometry and Computer Algebra Group about Boolean polynomial rings.

July 2006: Internal considerations about recent activities and ongoing work.

August 21-22 and 28-29 as well as September 4-5, 2006 : Series of joint working sessions of Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group, and Mathematisches Forschungsinstitut Oberwolfach consisting of organization and partial execution of joint software developments for formal verification of digital systems on bit-level.

September 26-29, 2006: Dr. Alexander Dreyer (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems)) presents interval methods for analog circuits at the SCAN 2006 in Duisburg.

September/October, 2006: Joint work of Reactive Systems Group and Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) about combining of interval arithmetic and hybrid automata for verification of properties of analog circuits.

October 12-13, 2006: Presentation of interval methods for analog circuits by Dr. Alexander Dreyer at the SMACD 2006 in Florence, Italy.

October 16-17 and 23-24, 2006: Visit of Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach): Joint implementation work and project briefing with Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Algebra, Geometry and Computer Algebra Group of methods for Gröbner bases over Boolean rings (at Fraunhofer Institute for Industrial Mathematics (ITWM)).

November 9, 2006: Presentation of the `PolyBoRi` framework for verification of Boolean expression systems by Algebra, Geometry and Computer Algebra Group and Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and delivery of the `PolyBoRi` framework for beta-testing purposes to Electronic Design Automation Group.

November 20-21, 2006: Project meeting and consultations between Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) at Fraunhofer Institute for Industrial Mathematics (ITWM).

December 1, 2006: Briefing about recent activities and ongoing work of Reactive Systems Group, Robotics Laboratory, Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Algebra, Geometry and Computer Algebra Group at the Department of Computer Science (Reactive Systems Group).

January 18, 2007 Talks in cooperation with project KryFoVe given by Martin Albrecht ("Algebraische Attacken auf Kryptosysteme", Bremen University) and Stanislav Bulygin ("Decoding linear codes via solving systems of polynomial equations") at Algebra, Geometry and Computer Algebra Group.

February 2, 2007 Project Meeting resuming activities and ongoing work of Reactive Systems Group, Robotics Laboratory, Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Algebra, Geometry and Computer Algebra Group at the Department of Computer Science (Reactive Systems Group).

February 19 and 26, 2007 Meeting for coordination of the preparation of the DASMOD-Workshop presentation by members of Reactive Systems Group, Robotics Laboratory, and Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) at the Department of Computer Science (Reactive Systems Group).

February 19 and 26, 2007 Meeting of Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Algebra, Geometry and Computer Algebra Group together with Mathematisches Forschungsinstitut Oberwolfach and Electronic Design Automation Group at the Department of Mathematics (Algebra, Geometry and Computer Algebra Group) for coordination ongoing work for digital systems verfication (PolyBoRi Framework).

February 28 - March 1, 2007 Presentation of VerSiS at the DASMOD Workshop.

March 5-8, 2007 Dr. Alexander Dreyer (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems)) presents combined methods using interval arithmetic and three-valued logic for verification of analog circuits at the 10. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" in Erlangen.

March 11-13, 2007 Poster presentation about three-Valued specification and verification of analog properties given by Dr. Raffaella Gentilini (Reactive Systems Group) at the 17th ACM Great Lakes Symposium on VLSI (GLSVLSI 2007) in Stresa - Lago Maggiore, Italy.

June 25-29, 2007 Software presentation of the PolyBoRi framework by Dr. Alexander Dreyer and Michael Brickenstein at Effective Methods in Algebraic Geometry (MEGA 2007) in Strobl, Austria.

November 11, 2007: Talk of Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) at SAGE Days 6 about the PolyBoRi framework.

November 22-23, 2007: Meeting for finalizing the first beta version of the PolyBoRi Framework (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group and Mathematisches Forschungsinstitut Oberwolfach).

January 30, 2008: Presentation of PolyBoRi's SCons-based build system at internal professional training seminar at Fraunhofer Institute for Industrial Mathematics (ITWM).

January 31, 2008: Presentation of PolyBoRi at the Seminar Cryptography und Computer Algebra at TU Darmstadt by Michael Brickenstein and Dr. Alexander Dreyer.

February 4, 2008: First release candidate for the second beta version of the PolyBoRi Framework (PolyBoRi 0.2 rc0). PolyBoRi 0.2 became available at February 22.

March 7, 2008: The release of PolyBoRi 0.3 contains several stability improvements, and a more simplified and standard-conforming build-process.

April 24, 2008: Talk of Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) about Gröbner-free Normal Forms for Boolean Polynomials at working group seminar of Algebra, Geometry and Computer Algebra Group (Department of Mathematics).

May 13, 2008: PolyBoRi 0.4 was released with a more exhaustive tutorial as well as several bug and stability fixed. Also, procedures for interreduction and partial function definition have been made available.

June 12, 2008: Oliver Wienand's talk Computer Algebra and Formal Verification at Algebra, Geometry and Computer Algebra Group (Department of Mathematics).

June 20 and 26, 2008: Meetings of Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) (Fraunhofer Institute for Industrial Mathematics (ITWM)), Algebra, Geometry and Computer Algebra Group (Department of Mathematics) and Electronic Design Automation Group (Department of Electrical Engineering and Information Technology) regarding the continuation of joint work about formal verification.

July 23, 2008: Talk about Gröbner-free Normal Forms for Boolean Polynomials by Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) at the ISSAC 2008 conference at Hagenberg, Austria.

August 13, 2008: Blackboard discussion at the Mathematisches Forschungsinstitut Oberwolfach about possible future cooperations of with Armin Biere (Institute for Formal Models and Verification at the Johannes Kepler University in Linz, Austria). Main subject was the combination of PolyBoRi and SAT solvers.

August 20, 2008: Work meeting of Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) and Electronic Design Automation Group (Department of Electrical Engineering and Information Technology) about automated formal verification using Gröbner techniques for foward/backward iterations.

September 23, 2008: PolyBoRi 0.5 comes with a revised user interface, which avoids some commonly mistaken features. Also, more standard conforming features regarding documentation and build tools were implemented. Finally, interfacing with an external M4RI library for Boolean linear algebra problems is possible now.

October 12, 2008: Presentation of the Secrets of Singular and PolyBoRi at Sage Days 10 by Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach).

November 5 and 12, 2008: Meetings of Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Algebra, Geometry and Computer Algebra Group about the integration of the PolyBoRi framework into the computer algebra system Singular.

November 20-21, 2008: Project meeting and consultations of Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach), Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Algebra, Geometry and Computer Algebra Group about upcoming PolyBoRi features and its integration into Singular.

Project Milestones

January 2006: Kick-off meetings and passing of the agendae.

March 2006: Presentations of the involved research groups' working areas and the state of the art of research areas.

March/April 2006: Starting concept and joint implementation for a Gröbner-basis approach for treating Boolean expressions (digital circuits verification) by Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group, and Mathematisches Forschungsinstitut Oberwolfach (external cooperation partner).

April 2006: Purposal of modelling a complete digital/analog system's signal path involving the techniques of all working groups. Its application example is simulation as well as formal verifikation of an outdoor robot (Robotics Laboratory).

May 2006: Exchange of techniques of the computer algebra tool SINGULAR (Algebra, Geometry and Computer Algebra Group), and the reactive systems verification tool AVEREST (Reactive Systems Group) is initiated.

September/October, 2006: Work about combination of interval arithmetic (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems)) and hybrid automata (Reactive Systems Group) for formal verification of analog circuits.

November 2006: Software framework PolyBoRi for Gröbner techniques over Boolean expressions is presented by Algebra, Geometry and Computer Algebra Group, Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), and Mathematisches Forschungsinstitut Oberwolfach.

December 2006: Resuming recent activities and ongoing work of all working groups.

February/March 2007: Presentations at the DASMOD workshop, MBMV workshop and the GLSVLSI symposium.

April-July 2007: Resumed activities in formal verification of digital systems, deepened cooperation with the PolyBoRi project (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group and Mathematisches Forschungsinstitut Oberwolfach).

August-October 2007: Summarized the results of the algebraic approach for Boolean equation systems. Preparation of a release candidate for digital system verification software (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group and Mathematisches Forschungsinstitut Oberwolfach).

November 2007: Presentation of PolyBoRi at SAGE days (Mathematisches Forschungsinstitut Oberwolfach). Release of the first beta version of the PolyBoRi Framework (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group and Mathematisches Forschungsinstitut Oberwolfach).

January - February 2008: Several presentations of the PolyBoRi framework (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Mathematisches Forschungsinstitut Oberwolfach). Release Candidates for the second beta version of the PolyBoRi Framework.

March - June 2008: Several beta versions of the PolyBoRi framework for computations in Boolean rings were released (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) and Mathematisches Forschungsinstitut Oberwolfach). Its user interface was revised, featured algorithms were added, extended and optimized, and a more exhaustive documentation including an online-tutorial was written. Furthermore, a standard conforming build process was completed.

June 2008: Strategic meetings of Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems) (Fraunhofer Institute for Industrial Mathematics (ITWM)), Algebra, Geometry and Computer Algebra Group (Department of Mathematics) and Electronic Design Automation Group (Department of Electrical Engineering and Information Technology).

April - July 2008: Theoretical and practical results were presented by Mathematisches Forschungsinstitut Oberwolfach and Algebra, Geometry and Computer Algebra Group at internal seminars and the ISSAC 2008 conference.

August 2008: Discussion about possible future cooperations (at Mathematisches Forschungsinstitut Oberwolfach and Department of Electrical Engineering and Information Technology).

September 2008: The revised beta version PolyBoRi 0.5 is available for download.

October/November 2008: Joint presentation of Singular and PolyBoRi at Sage Days 10. Integration of the PolyBoRi framework into the computer algebra system Singular started by Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems), Algebra, Geometry and Computer Algebra Group and Mathematisches Forschungsinstitut Oberwolfach.

Project Proposals

The following reports document some work-proposals resulting from our VerSiS Project workshops.

Project Workshops

The following presentations document results from the VerSiS Project.

Project Publications

Gröbner-free normal forms for Boolean polynomials

Michael Brickenstein, Alexander Dreyer. In: Proceedings of the twenty-first international symposium on Symbolic and algebraic computation (ISSAC '08), Linz/Hagenberg, Austria. ACM, New York, NY, USA, P. 55-62, July, 2008

New developments in the theory of Gröbner bases and applications to formal verification

Michael Brickenstein, Alexander Dreyer, Gert-Martin Greuel, Markus Wedler, Oliver Wienand. In: Special Issue of the Journal of Pure and Applied Algebra. Submitted, 2008

PolyBoRi: A Gröbner Basis Framework for Boolean Polynomials

Michael Brickenstein, Alexander Dreyer. Technical Report, Reports of Fraunhofer ITWM, Volume 122, Fraunhofer ITWM, August, 2007

PolyBoRi: A framework for Gröbner basis computations with Boolean polynomials

Michael Brickenstein, Alexander Dreyer. In: Electronic Proceedings of Effective Methods in Algebraic Geometry MEGA 2007. June, 2007

Formal Verification of Safety Behaviours of the Outdoor Robot RAVON

Martin Proetzsch, Tobias Schüle, Karsten Berns, Klaus Schneider. In: 4th International Conference on Informatics in Control, Automation and Robotics (ICINCO 2007). Submitted, May, 2007

Three-Valued Automated Reasoning on Analog Properties

Raffaella Gentilini, Klaus Schneider, Alexander Dreyer. In: 17th ACM Great Lakes Symposium on VLSI (GLSVLSI '07). Stresa-Lago Maggiore, Italy. ACM Press, P. 485--488, March, 2007

Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems

Raffaella Gentilini, Klaus Schneider, Alexander Dreyer. In: Christian Haubelt and Jürgen Teich ed., Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. Shaker Verlag, Aachen, Germany, P. 121--130, 10. Workshop MBMV '07, March, 2007

Series of Abstractions of Hybrid Automata for Monotonic CTL Model Checking

Raffaella Gentilini, Klaus Schneider, Bud Mishra. In: International Symposium on Logical Foundations of Computer Science (LFCS '07). New York, U.S.A.. LNCS, Springer, 2007

Resolving Parameter Dependences for Interval Analysis of Linear Analog Circuits

Alexander Dreyer. In: SMACD 2006 - International Workshop on Symbolic Methods and Applications to Circuit Design. Università degli Studi di Firenze, October, 2006

Automatische nichtlineare Verhaltensmodellgenerierung mit sequentieller Gleichungsstruktur

Daniel Platte, Ralf Sommer, Jochen Broz, Alexander Dreyer, Thomas Halfmann and Erich Barke. In: 9. ITG/GMM-Fachtagung Analog '06: Entwicklung von Analogschaltungen mit CAE-Methoden, Dresden. September, 2006 (in german)

Automatic Nonlinear Behavioral Model Generation using Sequential Equation Structures

Ralf Sommer, Daniel Platte, Jochen Broz, Alexander Dreyer, Thomas Halfmann and Erich Barke. In: SMACD 2006 - International Workshop on Symbolic Methods and Applications to Circuit Design. Università degli Studi di Firenze, September, 2006

Interval Analysis of Linear Analog Circuits

Alexander Dreyer. In: SCAN 06 - 12th GAMM - IMACS International Symposion on Scientific Computing, Computer Arithmetic and Validated Numerics. IEEE Computer Society Conference Publishing Services, Duisburg, Germany, ISBN-13: 978-0-7695-2821-2, September, 2006

Slimgb: Gröbner Bases with Slim Polynomials

Michael Brickenstein. In: Proceedings of RWCA'06, Basel. P. 55-66, March, 2006

Interval Methods for Analog Circuits

Alexander Dreyer. Technical Report, Berichte des Fraunhofer ITWM, Volume 97, Fraunhofer ITWM, 2006

r42 - 08 Dec 2008 - AlexanderDreyer

Copyright © University of Kaiserslautern, 2009. All material on this website is the property of the respective authors.
Questions or comments? Contact DASMOD webmaster.