Start of topic  Skip to actions
VerSiS: Verification and Simulation of Embedded Hybrid Systems
Project TopicThe purpose of the VerSiS Project is to add formal verification to the design process of reliable embedded systems.
Project DescriptionFormal 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 toleranceaffected components, together with new interval arithmetical approachs on the one hand, and modern modelling techniques for multiphysical 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
Scientific Personnel
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)
Algebra, Geometry and Computer Algebra Group (Department of Mathematics)
External Cooperation
Mathematisches Forschungsinstitut Oberwolfach
Electronic Design Automation Group (Department of Electrical Engineering and Information Technology)
Project KryFoVe
Project Events and AchievementsProject start: 01.10.2005 with a preliminary duration until the end of 2007
Project DatesEarly 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öbnerbasis approach for solving verification problems of digital circuits on bitlevel. 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 intervalmethods. 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 2122 and 2829 as well as September 45, 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 bitlevel. September 2629, 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 1213, 2006: Presentation of interval methods for analog circuits by Dr. Alexander Dreyer at the SMACD 2006 in Florence, Italy. October 1617 and 2324, 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 betatesting purposes to Electronic Design Automation Group. November 2021, 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 DASMODWorkshop 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 58, 2007 Dr. Alexander Dreyer (Sect. System Analysis, Prognosis and Control (formerly Sect. Adaptive Systems)) presents combined methods using interval arithmetic and threevalued logic for verification of analog circuits at the 10. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" in Erlangen. March 1113, 2007 Poster presentation about threeValued 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 2529, 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 2223, 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 SConsbased 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 standardconforming buildprocess. April 24, 2008: Talk of Michael Brickenstein (Mathematisches Forschungsinstitut Oberwolfach) about Gröbnerfree 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öbnerfree 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 2021, 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 MilestonesJanuary 2006: Kickoff 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öbnerbasis 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. AprilJuly 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). AugustOctober 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 onlinetutorial 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 ProposalsThe following reports document some workproposals resulting from our VerSiS Project workshops.
Project WorkshopsThe following presentations document results from the VerSiS Project.
Project Publications
Gröbnerfree normal forms for Boolean polynomialsMichael Brickenstein, Alexander Dreyer. In: Proceedings of the twentyfirst international symposium on Symbolic and algebraic computation (ISSAC '08), Linz/Hagenberg, Austria. ACM, New York, NY, USA, P. 5562, July, 2008New developments in the theory of Gröbner bases and applications to formal verificationMichael Brickenstein, Alexander Dreyer, GertMartin Greuel, Markus Wedler, Oliver Wienand. In: Special Issue of the Journal of Pure and Applied Algebra. Submitted, 2008PolyBoRi: A Gröbner Basis Framework for Boolean PolynomialsMichael Brickenstein, Alexander Dreyer. Technical Report, Reports of Fraunhofer ITWM, Volume 122, Fraunhofer ITWM, August, 2007PolyBoRi: A framework for Gröbner basis computations with Boolean polynomialsMichael Brickenstein, Alexander Dreyer. In: Electronic Proceedings of Effective Methods in Algebraic Geometry MEGA 2007. June, 2007Formal Verification of Safety Behaviours of the Outdoor Robot RAVONMartin Proetzsch, Tobias Schüle, Karsten Berns, Klaus Schneider. In: 4th International Conference on Informatics in Control, Automation and Robotics (ICINCO 2007). Submitted, May, 2007ThreeValued Automated Reasoning on Analog PropertiesRaffaella Gentilini, Klaus Schneider, Alexander Dreyer. In: 17th ACM Great Lakes Symposium on VLSI (GLSVLSI '07). StresaLago Maggiore, Italy. ACM Press, P. 485488, March, 2007Combining Interval Arithmetic and ThreeValued Temporal Logics for the Verification of Analog SystemsRaffaella 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. 121130, 10. Workshop MBMV '07, March, 2007Series of Abstractions of Hybrid Automata for Monotonic CTL Model CheckingRaffaella Gentilini, Klaus Schneider, Bud Mishra. In: International Symposium on Logical Foundations of Computer Science (LFCS '07). New York, U.S.A.. LNCS, Springer, 2007Resolving Parameter Dependences for Interval Analysis of Linear Analog CircuitsAlexander Dreyer. In: SMACD 2006  International Workshop on Symbolic Methods and Applications to Circuit Design. Università degli Studi di Firenze, October, 2006Automatische nichtlineare Verhaltensmodellgenerierung mit sequentieller GleichungsstrukturDaniel Platte, Ralf Sommer, Jochen Broz, Alexander Dreyer, Thomas Halfmann and Erich Barke. In: 9. ITG/GMMFachtagung Analog '06: Entwicklung von Analogschaltungen mit CAEMethoden, Dresden. September, 2006 (in german)Automatic Nonlinear Behavioral Model Generation using Sequential Equation StructuresRalf 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, 2006Interval Analysis of Linear Analog CircuitsAlexander 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, ISBN13: 9780769528212, September, 2006Slimgb: Gröbner Bases with Slim PolynomialsMichael Brickenstein. In: Proceedings of RWCA'06, Basel. P. 5566, March, 2006Interval Methods for Analog CircuitsAlexander Dreyer. Technical Report, Berichte des Fraunhofer ITWM, Volume 97, Fraunhofer ITWM, 2006
