November 12th, 2019 - Mehran Goli successfully defended his dissertation. Modeling electronic systems as Virtual Prototypes (VPs) using SystemC language at the Electronic System Level (ESL) has become an industry-accepted solution over the last decade. However, lack of proper VP analysis methodologies and tools to tackle various tasks in the design process such as design understanding, verification, debugging, or design space exploration are still a major issue. In his thesis, Mehran Goli addresses this problem by providing an automated and comprehensive design understanding methodology, enabling designers to analyze a given Vp from two perspectives: debugger-based and compiler-based approaches. Focusing on applications is the second part of his dissertation, which pays off the key benefits of a strong design understanding methodology. Mehran Goli shows how the results of the first part can be used as a starting point for various applications in the design process, such as verification, security validation, and design space exploration

From September 3 to 4, 2019, Mehran Goli attended the ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) which was held in Alberta, Canada. Mehran presented the paper "Integrating Hybrid Analysis with Machine Learning Techniques for Portion Resilience Evaluation in Approximating SystemC-based Designs". The proposed approach effectively guides designers to know under which error limits different portions of a given SystemC design at different granularity levels (i.e., from a single statement to a module) can be approximated.

Mehran Goli attended the EUROMICRO Digital System Design Conference (DSD) which was held in Kallithea - Chalkidiki, Greece, from August 28 to 30, 2019. Mehran presented the paper "Scalable Simulation-based Verification of SystemC-based Virtual Prototypes" which proposes a Scalable simulation-based verification approach, enabling designers to check the validity of a given SystemC-based VP against the VP¿s specification (i.e. functionality and timing behavior) and TLM-2.0 rules.

From June 2nd to 6th 2019, Rehab Massoud attended the 56th Design Automation Conference (DAC) which was held at Las Vegas this year. Rehab presented the paper "Temporal Tracing of On-Chip Signals using Timeprints" which proposes timeprints as a new light-weight, yet cycle-accurate signal traces, that can be logged from Cyber-Physical Systems while operating in field. Being of extreme light-weight, timeprints open the door for the first time to a wide range of deployment-phase accurate timing-properties verification. Moreover, she presented her PhD topic "Timeprints-based Verification" at the DAC PhD forum.

Alireza Mahzoon attended the International Workshop on Logic and Synthesis (IWLS) which was held in Lausanne, Switzerland, from June 20 to 22, 2019. Alireza presented the paper "GenMul: Generating architecturally complex multipliers to challenge formal verification tools". GenMul is an open source multiplier generator which outputs multiplier circuits in Verilog with configurable architectures and input sizes. GenMul allows to challenge the existing formal verification techniques particularly Symbolic Computer Algebra (SCA) based verification methods and to study the reason for verification failure of non-trivial multipliers.

Arithmetic circuits such as multipliers occur today in every processor. If they contain a bug, this causes very high costs. Hence, ensuring the functional correctness of these circuits in a strong mathematical sense is inevitable.

For the paper entitled "PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers" Alireza Mahzoon, Dr. Daniel Große and Prof. Dr. Rolf Drechsler received the Best Paper Award on November 5, 2018 at the International Conference on Computer Aided Design (ICCAD), one of the top conferences in circuit design in San Diego, USA.

The paper introduces a verification method based on Symbolic Computer Algebra (SCA) and presents a new theory for the origin of vanishing monomials, redundant monomials which lead to an monomial explosion for non-trivial multipliers. The implemented SCA-verifier PolyCleaner is able to prove the correctness for non-trivial million-gate multipliers where the other state-of-the-art methods failed.

October 1st, 2018 - Saeideh Shirinzadeh sucessfully defended her dissertation targeting in-memory computing, an emerging computing paradigm which allows to perform computation within memory devices. This is in contrary to today's computer architectures, where the data is processed and stored in two separate units. This needs communication between processor and memory which causes high latency and therefore lowers the performance. In her thesis, Saeideh Shirinzadeh addresses this problem by proposing design approaches for in-memory computing using an advanced non-volatile memory technology. She has proposed a comprehensive framework for development and automation of efficient logic-in-memory computing hardware and computer architecture which can potentially provide several orders of speed-up for emerging applications dealing with massive amounts of data.

From August 27th to 30th 2018, Anika Behrens attended the 13th International Conference on Availability, Reliability and Security (ARES 2018). The conference was held in Hamburg, Germany. Anika Behrens presented a paper entitled "What are Security Patterns? A Formal Model for Security and Design of Software" providing a formal definition of security patterns suitable for automated processes, such as code generation, or code verification. She demonstrated that security patterns theoretically lead to formal constraints that range over all Chomsky types and showed how formal security patterns of Chomsky type 3 can be reduced to particular expressions under some assumptions.

From July 8th to 11th 2018, Alireza Mahzoon attended the IEEE Computer Society Annual Symposium on VLSI (ISVLSI), which was held in Hong Kong, China. Alireza presented the paper "Combining Symbolic Computer Algebra and Boolean Satisfiability for Automatic Debugging and Fixing of Complex Multipliers", which proposes a complete debugging flow based on the combination of Symbolic Computer Algebra (SCA) and Boolean Satisfiability (SAT) for non-trivial multipliers. The proposed approach consists of three phases: arithmetic circuit verification, bug candidates localization, and finally design fixing.

From May 15th to 18th 2018, Saeideh Shirinzadeh attended ISMVL 2018, the IEEE International Symposium on Multiple-Valued Logic which was held in Linz, Austria. Saeideh Shirinzadeh presented a tutorial paper which was a joint international collaboration between University of Bremen and National Institute of Technology Meghalaya in India. The tutorial is entitled "Logic Design using Memristors: An Emerging Technology" and introduced the state-of-the-art for synthesis of circuits and hardware using memristor, which is a non-volatile memory technology allowing to perform logic primitives.

January 10, 2018 - "Is it possible to completely test reactive Systems with inputs from an infinite input domain?" This question has been addressed in the PhD thesis of Felix Hübner. Therefore, Felix Hübner applied a complete model-based testing approach to the railway domain. The approach is based on an input equivalence class partitioning. Under the assumption that certain test hypotheses hold, it is ensured that all potential errors in the system under test are detected. Felix Hübner was particularly interested in the error detection capabilities of the applied approach for real-world errors for which the test hypotheses are usually violated.

For the evaluation of the error detection capabilities, Felix Hübner implemented a novel mutation analysis approach which introduces artificial errors to a SystemC-model to mimic typical HW/SW integration errors. In his work he provides experimental results that show the adequacy of the approach considering several case studies. Finally, Felix Hübner could demonstrate that a combination of the equivalence class approach with randomisation and boundary-value selection is able to significantly increase the probability to detect HW/SW integration errors.

From September 4th to 7th, Rehab Massoud will attend FORMATS-2017, the 15th International Conference on Formal Modelling and Analysis of Timed Systems, which is held this year in Berlin. Rehab will present the paper "Semi-Formal Cycle Accurate Temporal Traces Reconstruction", which proposes an approach for tracing of on-chip transactions by separating the concerns "Temporal" and "Functional" into two tasks, logging footprints of designated monitored on-chip execution to retrieve accurate timing information and high level functional simulation to retrieve signal contents. A semi-formal cycle-accurate reconstruction method is then used to retrieve a complete, cycle-accurate trace of a given signal.

"Can we fix the bit errors in the processors of a space satellite more efficiently with error detection and recomputation?" In his research, Gökçe tried to answer this question.

In radiation environment like space or nuclear reactor, electronics can fail due to bitflips in processors. A common solution is the triple modular redundancy (TMR), in which every memory bit is triplicated. If one of the three bits is flipped, then the bit can be recovered by looking at the other two bits.

TMR results in threefold extra processor area, slower processing speed, and increased energy consumption. Gökçe evaluated an alternative data processing scheme, where the data processing is divided in many parts, and the part is processed again if a bit flips.

His results show that the alternative method can save up to the half of the extra processor area that would be needed by the TMR. This area saving can be the key for fitting more applications to a space-constrained chip.

August 17, 2017 - Dr. Matthias Goldhoorn was dealing with the efficient modelling of robotic system behaviors. He designed, developed and programmed the robotic system "Avalon" (Autonomous Vehicle for Aquatic Learning, Operation and Navigation) to support the analysis of this problem. The analysis led to a complete new concept to design component networks on a model based approach to describe system behaviors. By using constrained base methods, a robotic system is now able to fulfill missions in a robust, verifiable and efficient manner. Due to his research, the system "Avalon" was capable to win the underwater contest SAUC-E in the year 2014.

26.07.2017 - The goal of Malgorzata's Goldhoorn dissertation was to develop an approach by means of which the prediction of the most probable object location can be made. A robotics system, such as an assistance robot, could make use of this information in order to find a given object in the environment.

For this purpose, Malgorzata defined a formalism for Probabilistic Qualitative Spatial Relations (PQSR). By means of this formalism, spatial knowledge about typical relations between objects can be modelled in a probabilistic and qualitative manner. Based on the PQSR, the Spatial Potential Field (SPF) were developed, and in turn, used for calculation of the most probable objects position.

This theoretical approach was applied to real world data in order to evaluate its applicability for robotics purposes. The resulting validation demonstrates that the developed method performs well and can be used for object search purposes.

Saeideh Shirinzadeh attends the Genetic and Evolutionary Computation Conference (GECCO) from 15th-19th July in Berlin. She presents her paper entitled "An Adaptive Prioritized ε-Preferred Evolutionary Algorithm for Approximate BDD Optimization" proposing an evolutionary approach to improve the efficiency of BDDs by incorporating optimization and approximation.

In his PhD thesis Nils Przigoda dealt with validation and verification of UML/OCL models using formal methods by means of SMT solvers. For this purpose, a general technique has been developed which translates UML/OCL models into a valid input for SMT solver. This process is called model transformation or short transformation. On this basis different approaches for the validation and verification of structural as well as behavioral aspects of UML/OCL models have been realized. One approach determines all minimal reasons for non-instantiable models, i.e., the contradiction between the model elements are identified. Another approach deals with the concurrent execution of operations. Furthermore, it is shown in the thesis that the proposed approaches can be transferred to tackle other research areas. This is exemplarily demonstrated by means of timing properties of MARTE/CCSL models (a UML2 profile). Finally, an approach verifying an implementation against the pre- and postconditions of the model is introduced. Overall, the thesis presents several approaches to validate and verify models before any implementation steps are done and also shows how this results can be transferred to the next level within the system design flow.

From March 27 to 31, Mehran Goli was at the Design, Automation and Test in Europe (DATE) which was held in Lausanne. He presented his paper entitled "Automatic Equivalence Checking for SystemC-TLM 2.0 Models Against their Formal Specifications" where he described a state-of-the-art approach to verify a given SystemC model against its formal specification.

From March 27 to 31, Saeideh Shirinzadeh was at the Design, Automation and Test in Europe (DATE) which was held in Lausanne. She presented her research work at the PhD forum of the conference as well as a paper entitled "Endurance Management for Resistive Logic-in-Memory Computing Architectures" where she proposed techniques to manage an emerging memory technology.

His dissertation is about estimating poses from inertial sensor data, that is estimating orientations and positions. This includes poses of single rigid bodies as well as poses of systems of jointed rigid bodies, e.g. postures (of skeletons) of humans. The rotation of a single body around the vertical is unobservable form inertial sensor data only. To determine the (human) posture with all degrees of freedom of the skeleton's limbs’ relative poses, the acceleration and angular velocity measurements are fused with prior knowledge about the structure of the skeleton. The algorithm is used in the motion capturing workwear "SIRKA" to estimate postures of manual workers, for instance in shipbuilding, where conventional approaches, e.g. determining the rotation around the vertical using magnetometers, are impractical.

Goal of his work was the development of an optimal controller for an entertainment robot called "Doggy" (due to his costum), to rebound a ball. The task of beeing at a defined time at a defined position with the defined velocityto rebound the ball has been integrated into an LQR cost function. Moreover, physical constraints has been integrated as costs. The control algorithm is devided into a linear and nonlinear part. The linear part runs with 5 times higher frequency on a microcontroller then the nonlinear part on a PC. This is a new technique in control theory, which solves a task under real-time conditions.
Moreover, the robot has been calibrated to get a model for the controller and for a state estimator, which also runs on the mocrocontroller. The calibration and the real-time state estimator has also been a contribution.

Niels Thole successfully defended his PhD. The title of his thesis is "Formal Verification throughout the Development of Robust Systems". He worked on equivalence checking in the refinement from high-level models as well as approaches for transient error detection at the gate-level using formal methods.

Congratulations!

Eleonora Schönborn successfully defended her PhD on September 21st, 2016. Her thesis is entitled "Scalable Design and Synthesis of Reversible Circuits". In her research she focused on the design of reversible circuits which can be used for quantum circuits. She developed new methods to design such circuits based on programming languages. From theses descriptions circuits can be automatically synthesized.

Congratulations!

From the 11th - 13th July Niels Thole was at the conference IEEE Computer Society Annual Symposium on VLSI (ISVLSI) in Pittsburgh. During this event, he presented his paper "A Hybrid Algorithm to Conservatively Check the Robustness of Circuits" where he described a state-of-the-art approach to analyze the robustness of a circuit against transient faults.

Felix Hübner participated in the International Conference Reliability, Safety and Security of Railway Systems (RSSR2016) in Paris, which took place from 28th to 30th of June 2016. The conference aims at bringing together experts of formal methods in the railway domain. Felix Hübner is co-author of the article "A Novel Approach to HW/SW Integration Testing of Route-Based Interlocking System Controllers", which was presented at RSSR2016.

Judith Peters successfully defended her PhD on December, 18th 2015. Her thesis is entitled "Exploiting MARTE / CCSL in Modern Design Flows". Dr. Judith Peters worked on the specification and verification of the timing behavior of complex systems. For this task she exploited the usage of formal timing descriptions in system design.
Congratulations!

Gökçe Aydos presents his work at NORCAS 2015
Can parity-based error detection protect a digital circuit against soft
errors in an area-efficient manner? Last October, PhD student Gökçe
Aydos presented his empirical results at NORCAS (Nordic Circuits and
Systems Conference) in Oslo.

05.10.2015 – This Monday, Melanie Diepenbeck successfully defended her PhD. The title of her thesis is "Completing behavior-driven development for Testing and Verification". She completed her PhD as the third scientist in the Graduate School.

On 11th of July 2015 the OPEN CAMPUS day of the University of Bremen took place. Dennis Schüthe from the graduate school SyDe presented his ball playing robot Doggy for the first time. The robot gathered a crowd of interested visitors, young and old alike. Doggy appeals to a wide audience: While children like to play with the robot in his funny costume, the electronics under the hood inspire the technically interested spectators.

20.07.2015 – This Monday, Julia Seiter successfully defended her PhD. The title of her thesis is "Formal Model Refinement - From Specification to Implementation". She completed her PhD as the second scientist in the Graduate School.
Congratulations!

Dennis Schüthe and Felix Wenk presented their recent works at the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS).

IROS is an annual academic conference covering advances in robotics. It is one of the premier conferences of its field.
Topics range from computer vision, sensor fusion, (optimal) robot control, human-robot interaction to designing and building robots and their applications.

IROS 2015 took place in Hamburg from October 28th until November 2nd.

Dennis Schüthe presented "Optimal Control with State and Command Limits for a Simulated Ball Batting Task", which is an enhancement of the predeveloped controller without limitations. Thus, the controller knows the physical limitations of the robot and is able to move the motors optimally around in the workspace to hit a ball back to a desired goal.
This is done without any trajectory planning, the controller itself takes care of it by adapting to the situation, which is the most advantage.

Felix Wenk presented "Posture from Motion", a technique to reconstruct the body posture of the bearer of an inertial measurement suit. Estimating the 3-dimensional orientation of an individual body segment is impossible without complementary sensors. By broadening the scope of the estimator to all segments of the skeleton whose posture is to be reconstructed, the skeleton's structure can be used to compute the relative orientations of all body segments from the suit bearer's motion.

The conference Test and Proof (TAP) takes place for the ninth time in 2015 and considers the synergy and combination of techniques from the fiels of testing and verification. This year, the TAP conference takes place at L'Aquila in Italy. Julia Seiter will present the work "Coverage of OCL Operation Specifications and Invariants" which discusses how to check completeness at formal specification level.

As the only junior researcher from Bremen, the Ph.D. candidate Judith Peters has not just gained the A. Richard Newton Young Fellow Award by the Design Automation Conference (DAC), she also got the possibility to introduce her work and to discuss it with a chosen circle of internationally well-known researchers within the Ph.D. Forum of the five-days long conference located in San Francisco. Both awards include funding of in total nearly 2,000 Euro. The DAC 2015 can be seen as the globally most important conference for researchers addressing the design of circuits and systems. More than 7,000 visitors are expected for the event between June 7th and 11th, 2015. To accompany her during her stay at DAC visit facebook at https://www.facebook.com/LadyNinkharsag where she is going to blog about her experiences.

How can robots find and recognize objects? How can electronic equipment resist the strong vibrations during a space shuttle launch? How can we assure and improve the quality of technical systems that are used in everyday life? These questions are among the research topics of the PhD students in the Graduate School System Design. In the new video clip of the university of Bremen, the spokesman professor Rolf Drechsler and the scientific coordinator Ulrich Kühne present the Graduate School, and some of the PhD students explain their work. The clip is part of a series of videos which have been produced by the University of Bremen's Press Relations Office and the Media Services (ZMML). They give insight into the projects which are funded by the German Excellence Initiative.

Starting in March 2015, Niels Thole will spend his time with the researchers at the TIMA institute in Grenoble. This research stay is funded by the German Academic Exchange Service (DAAD), where Niels successfully applied for a six month scholarship.
In his thesis, Niels investigates the resilience of hardware systems against transient errors. Such errors play an important role in systems which are exposed to strong radiation, such as in satellites and space vehicles. But also down on earth, they occur more and more frequently due to the continuously shrinking transistors within integrated circuits, which makes them more vulnerable to radiation events.
The host institute TIMA in Grenoble has more than 100 employees in four research groups, which are working on the analysis of hardware-related properties of electronic systems. Here, Niels will integrate with the AMFORS group, bringing together his current research with the strong know-how of the TIMA lab. This will allow a more detailed analysis of the effects of transient faults.
In October last year, Niels applied for a six month scholarship within the program FITworldwide by DAAD. With this funding line, the German Academic Exchange Service supports master students, PhD students, and postdocs in the field of computer science. The goal is to improve the mobility of young researchers from Germany.

I'm developing the the sensor fusion and posture estimation of the motion capturing suit SIRKA. SIRKA (mostly) looks and feels like normal workwear as used at the Meyer Werft and the Johanniter Unfallhilfe, while it continuously estimates the wearer's posture.

The primary research challenge — which I'm currently working on — is the restriction to inertial sensors, which will allow the suit to be used in environments previously deemed impractical.

We also developed a prototype sensor network, which uses additional magnetometers. The prototype is used for developments building on the posture estimate and was also presented at this year's CeBIT.

The paper utilizes the "Modeling and Analysis of Real-Time and Embedded Systems" (MARTE) profile of the "Unified Modeling Language" (UML), which especially enables for a modeling of embedded systems. These are normally composed by several modules. MARTE offers a language to specify timing, the "Clock Constraint Specification Language" (CCSL). The paper is about the generation of a generic abstraction of it, which can be utilized in various fashions during system design and development. In particular, the verification and its feasability is demonstrated by some example.

In December 2014, a new booklet about the Graduate School System Design has been published. It presents all important information on the PhD program and its partner institutions. The leaflet will help students who are interested in starting a PhD within SyDe.

The FDL is conference with a focus on design and specification languages which will take place from October 14 till October 16 in Munich. Julia Seiter will present her work on Automatic Refinement Checking for Formal System Models which is also nominated for the Best Paper Award. Furthermore, a joint work with Christoph Hilken will be published under the title Verifying Consistency between Activity Diagrams and Their Corresponding OCL Contracts.

For the 2014 summer school, the Graduate School System Design went on a three days retreat in the coastal region north of Bremen. Apart from the day-to-day university business, the PhD students had the opportunity to attend to interesting lectures and to get to know new software tools during interactive tutorials. As speakers, both researchers of the University of Bremen and experts from industry were invited. Two software architects from Mentor Graphics presented the daily challenges in developing large and heterogeneous software systems in the industrial practice. The German Aerospace Center provided exciting insights into the planning and realization of a real space mission. In a hands-on session, the participants learned to model and test real-time embedded systems. But they also had to take action themselves: Each of the PhD students held a short presentation in the style of PechaKucha. Following this format, each talk consists of 20 slides, each of which lasts exactly 20 seconds. While this task is indeed challenging for the presenter, the results were remarkably entertaining.

The International Conference on Engineering of Complex Computer Systems (ICECCS,http://cs.tju.edu.cn/iceccs/2014/index.jsp) is a
well-known conference in the field of system design and engineering.
The 2014 conference was the 19th happening of it and took place in Tianjin, China. Ms Peters was introducing there her paper "Generating SystemC Implementations for Clock Constraints specified in UML/MARTE CCSL".

This addresses the generation of code from descriptions of timing and temporal behaviour, which are provided in a formal way (UML/MARTE CCSL).
From the decriptions basing on clocks SystemC code for simulation is generated.

The Graduate School System Design (SyDe) is going to grow by recruiting international PhD students. Thanks to the German Academic Exchange Service (DAAD), SyDe acquired funding for a total of four scholarships for excellent students from abroad.

On Friday, 13th of December, Mehdi Dehbashi will be the first of the Graduate School System Design to defend his PhD. The topic of his thesis is "Debug automation from pre-silicon to post-silicon". He will successfully finish his doctorate after just three years under the guidance of Prof. Görschwin Fey.

In the beginning of 2014, Eleonora Schönborn, PhD student in SyDe, will spend one month at the Bengal Engineering and Science University. The research stay is organized in the course of an DST-DAAD exchange project. Eleonora will collaborate with researchers in India to create a new design process for the computer of tomorrow. Already now, she is working with an Indian colleague in the field of reversible logic.