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)
Robotics Laboratory (Department of Computer Science)
Algebra, Geometry and Computer Algebra Group (Department of Mathematics)
- Dipl.-Math. Oliver Wienand
External Cooperation
Mathematisches Forschungsinstitut Oberwolfach
Electronic Design Automation Group (Department of Electrical Engineering and Information Technology)
- Dr.-Ing. Markus Wedler
- Evgeny Pavlenko
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
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
Michael Brickenstein, Alexander Dreyer, Gert-Martin Greuel, Markus Wedler, Oliver Wienand. In:
Special Issue of the Journal of Pure and Applied Algebra. Submitted, 2008
Michael Brickenstein, Alexander Dreyer. Technical Report, Reports of Fraunhofer ITWM, Volume 122, Fraunhofer ITWM, August, 2007
Michael Brickenstein, Alexander Dreyer. In:
Electronic Proceedings of Effective Methods in Algebraic Geometry MEGA 2007. June, 2007
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
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
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
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
Alexander Dreyer. In:
SMACD 2006 - International Workshop on Symbolic Methods and Applications to Circuit Design. Università degli Studi di Firenze, October, 2006
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)
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
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
Michael Brickenstein. In:
Proceedings of RWCA'06, Basel. P. 55-66, March, 2006
Alexander Dreyer. Technical Report, Berichte des Fraunhofer ITWM, Volume 97, Fraunhofer ITWM, 2006
