Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2016 | Buch

Automatic Refinement Checking for Formal System Models Kapitel lesen Erstes Kapitel lesen

Languages, Design Methods, and Tools for Electronic System Design

Selected Contributions from FDL 2014

herausgegeben von: Frank Oppenheimer, Julio Luis Medina Pasaje

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Electrical Engineering

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book brings together a selection of the best papers from the seventeenth edition of the Forum on specification and Design Languages Conference (FDL), which took place on October 14-16, 2014, in Munich, Germany. FDL is a well-established international forum devoted to dissemination of research results, practical experiences and new ideas in the application of specification, design and verification languages to the design, modeling and verification of integrated circuits, complex hardware/software embedded systems, and mixed-technology systems.

Inhaltsverzeichnis

Frontmatter

Formal Models and Verification and Predictability

Frontmatter
Chapter 1. Automatic Refinement Checking for Formal System Models
Abstract
For the design of complex systems, formal modelling languages such as UML or SysML find significant attention. The typical model-driven design flow assumes thereby an initial (abstract) model which is iteratively refined to a more precise description. During this process, new errors and inconsistencies might be introduced. In this chapter, we propose an automatic method for verifying the consistency of refinements in UML or SysML. For this purpose, a theoretical foundation is considered from which the corresponding proof obligations are determined. Afterwards, they are encoded as an instance of satisfiability modulo theories (SMT) and solved using proper solving engines. The practical use of the proposed method is demonstrated and compared to a previously proposed approach.
Julia Seiter, Robert Wille, Ulrich Kühne, Rolf Drechsler
Chapter 2. Towards Simulation Based Evaluation of Safety Goal Violations in Automotive Systems
Abstract
With the advent of the ISO 26262 it became crucial to prove that electrical and electronic products delivered into safety-related automotive applications are adequately safe. For this purpose safety goal violations due to random hardware faults need to be evaluated. In order to gain evident results for argumentation within the evaluation, a fault injection based approach is utilised. Potential risk scenarios are initiated by injection of analogue and digital faults into the heterogeneous behavioural model which comprises the safety-related hardware. For fault injection in heterogeneous models, we propose analogue saboteurs, designed in VHDL-AMS, by which amongst electrical or mechanical, diverse energy domain analogue hardware faults may be injected. For demonstration of this approach, a hardware model, comprising lithium-ion battery cells with a cell balancing and monitoring module and safety-related circuitry is used.
Oezlem Karaca, Jerome Kirscher, Linus Maurer, Georg Pelz
Chapter 3. Hybrid Dynamic Data Race Detection in SystemC
Abstract
Data races are one of the most common problems in concurrent programs. As SystemC standard allows nondeterministic scheduling of processes, this leads to many concurrency problems. Data races are the most commonly encountered concurrency problems and they need to be detected for improving SoC design quality. Different executions of the same concurrent program may lead to unexpected results due to race conditions. We develop a hybrid dynamic data race detection algorithm for SystemC/TLM designs that adopts the well-studied dynamic race detection algorithms; lockset and happens-before. We develop a segment-based technique where a segment is defined as a set of consecutive memory accesses by a single thread. Experiments show that our solution has fewer false positives than lockset and fewer false negatives than happens-before algorithms. Our implementation uses dynamic binary instrumentation allowing us to work on designs for which source codes may not be available such as pre-compiled IPs.
Alper Sen, Onder Kalaci

Languages for Requirements

Frontmatter
Chapter 4. Semi-formal Representation of Requirements for Automotive Solutions Using SysML
Abstract
As system complexities are growing with increasing numbers of requirements, the difficulties to manage, process and verify natural language requirements and to keep quality are also increasing. In safety-related applications, as in the automotive domain, this necessity is more pronounced because of the regulations and standards imposed by authorities. Semi-formal representation of requirements is an approach that helps making them more understandable and rigorous.
This chapter deals with semi-formal representation using SysML of two automotive analogue-mixed signal systems, an electronic power switch and an airbag safety circuit. We use diagram-based modelling in order to represent requirements, structure and behaviour, enabling the linking different elements that define the composition and the functionalities of the desired product. We focus on the particular behaviour of such devices and the continuous quantities related to them with emphasis on the two real scenarios.
Liana Muşat, Markus Hübl, Andi Buzo, Georg Pelz, Susanne Kandl, Peter Puschner
Chapter 5. A New Property Language for the Specification of Hardware-Dependent Embedded System Software
Abstract
This work introduces a new property language for describing the behaviour of low-level hardware-dependent software. The design of the language is motivated by the industrial success of property languages for hardware verification by simulation and formal techniques. The new language is constructed to concisely capture the timed behaviour of the interactions between software and hardware by means of sequences. In this chapter we present how the proposed verification language can be used to perform formal verification based on a computational model called program netlist. We show how the sequence model of the language is synthesised and combined with the program netlist so that a unified formula for a decision procedure, e.g., a SAT solver, can be constructed. Furthermore, a method for coverage analysis of property sets is introduced. The coverage criterion we propose determines whether or not the property set completely describes the input/output functional behaviour of a program. The work presents a case study showing how to use the proposed property language in order to specify an industrial implementation of a LIN (Local Interconnect Network) bus driver.
Binghao Bao, Carlos Villarraga, Bernard Schmidt, Dominik Stoffel, Wolfgang Kunz
Chapter 6. Exploiting Electronic Design Automation for Checking Legal Regulations: A Vision
Abstract
Legal regulations are large and complex documents that require experts such as lawyers to be understood. Working with these documents is a manual and time- consuming task. Common use cases are to decide whether a submission is conform with the regulations or to check whether certain corner cases are possible in the given set of rules. We envision to address many of these problems by treating legal regulations in the same manner as system specifications. This allows to apply sophisticated formal methods from Electronic Design Automation (EDA). For this, we briefly discuss the process of (semi)-automatically formalizing legal regulations. Afterwards, we illustrate the correspondence of various problems in the considered domain (here: regulations on scales and fees for medical doctors) with well-known EDA problems. We sketch the application of formal methods by means of examples and envision that in the future, the exploitation of formal methods to analyse legal regulations will greatly help lawmakers and “end users” alike.
Oliver Keszocze, Robert Wille

Parallel Architectures

Chapter 7. Synthesizing Code for GPGPUs from Abstract Formal Models
Abstract
Today multiple frameworks exist for elevating the task of writing programs for GPGPUs, which are massively data-parallel execution platforms. These are needed as writing correct and high-performing applications for GPGPUs is notoriously difficult due to the intricacies of the underlying architecture. However, the existing frameworks lack a formal foundation that makes them difficult to use together with formal verification, testing, and design space exploration. We present in this chapter a novel software synthesis tool—called f2cc—which is capable of generating efficient GPGPU code from abstract formal models based on the synchronous model of computation. These models can be built using high-level modeling methodologies that hide low-level architecture details from the developer. The correctness of the tool has been experimentally validated on models derived from two applications. The experiments also demonstrate that the synthesized GPGPU code yielded a 28× speedup when executed on a graphics card with 96 cores and compared against a sequential version that uses only the CPU.
Gabriel Hjort Blindell, Christian Menne, Ingo Sander
Chapter 8. A Framework for Distributed, Loosely-Synchronized Simulation of Complex SystemC/TLM Models
Abstract
Today’s virtual prototypes model complex many-core platforms. In application domains such as network processing, they may comprise hundreds of processors, which makes simulation speed the key issue due to the single-threaded execution semantics of SystemC. We propose CoMix, the Concurrent Model Interface, for the distributed simulation of large-scale SystemC models. CoMix provides robust communication between simulator peers, enables their loose synchronization, and manages the overall life cycle. It is an overlay technology neither requiring modified simulators nor depending on a hosts’ communication infrastructure. The CoMix framework is small (2k Lines of C++ Code) and easily deployable. We quantify its overhead on synthetic benchmarks and observe reasonable speedups for synthetic benchmarks as well as a large real-world example, e.g., 3.3X and 4X for a 4-peer simulation.
Christian Sauer, Hans-Martin Bluethgen, Hans-Peter Loeb

Modelling and Verification of Power Properties

Frontmatter
Chapter 9. Towards Satisfaction Checking of Power Contracts in Uppaal
Abstract
Since energy consumption is one of the most limiting factors for embedded and integrated systems, today’s microelectronic design demands urgently for power-aware methodologies for early specification, design-space exploration, and verification of the designs’ power properties. To this end, we currently develop a contract- and component-based design concept for power properties, called power contractss, to provide a formal link between the bottom-up power characterization of low-level system components and the top-down specification of the systems’ high-level power intent. In this paper, we present a first proof of concept for the verification of the leaf-component power contracts of a hierarchical system design w.r.t. their implementation in UPPAAL. Building on these, we can provide assured power contracts for the hierarchical virtual integration (VI) of the leaf-components to a compound power contract of the integrated final system and thus allow for a sound and traceable bottom-up integration and verification methodology for power properties.
Gregor Nitsche, Kim Grüttner, Wolfgang Nebel
Chapter 10. SystemC AMS Power Electronic Modelling with Ideal Instantaneous Switches
Abstract
Ideal instantaneous switches are a useful behaviour abstraction technique for modelling semiconductor components in power system development. This behaviour abstraction allows fast and robust simulations of sophisticated power systems. In this paper, we present a SystemC AMS extension that supports ideal switches modelling and simulation. Using this extension, large externally and internally controlled electrical linear networks can be integrated into system level models for design and verification purposes. To validate our implementation, we modelled and simulated a complex high voltage power converter for medical applications. The results demonstrate the robustness and accuracy of our SystemC AMS extension.
Leandro Gil, Martin Radetzki
Metadaten
Titel
Languages, Design Methods, and Tools for Electronic System Design
herausgegeben von
Frank Oppenheimer
Julio Luis Medina Pasaje
Copyright-Jahr
2016
Electronic ISBN
978-3-319-24457-0
Print ISBN
978-3-319-24455-6
DOI
https://doi.org/10.1007/978-3-319-24457-0

Neuer Inhalt

    Bildnachweise