English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Inmany of today’s technical appliances, embedded systems are deployed on an increasing scale. This trend is expected to massively gain in importance, especially for applications in consumer and automotive electronics, telecommunications, medical engineering, and avionics. Embedded systems can be characterized as follows: • They mostly consist of both hardware and software and perform control or communication tasks within an overall system, to which they are connected via networks, sensors, and actors. • In general, they are heterogeneous, often distributed systems with realtime requirements which may work on both transformative and reactive domains. • They typically are not directly visible to the user who interacts unconciously with them. The design of embedded systems poses significant challenges since system complexity grows rapidly. In particular, very elaborate design methods are necessary, and quality requirements are high because embedded systems often realize safety-critical functions. Hence the use of design automation tools has become indispensable. These can—based on a formal representation—analyze system properties and prove the correctness of the design. Then the implementation can be synthesized by automatically generating hardware and software descriptions. This enables a more flexible, faster, and less expensive design process than without automation. Within this context, the following topics are subject of this monograph: • A formal representation model called FunState is introduced which is especially suited to support embedded systems design. FunState serves as an internal design representation and can be used for modeling mixed hardware/software systems for analysis and synthesis purposes. • Based on FunState , a formal verification approach is presented which makes it possible to automatically check whether desired system properties are satisfied. In contrast to conventional verification techniques, formal verification can prove the correctness of a system’s model mathematically. ii Abstract  • In order to generate an implementation, the execution order of functional parts within the system has to be determined, often in compliance with additional constraints. A novel, FunState-based approach to this so-called scheduling is explained. For the above-mentioned applications, mainly symbolic methods based on interval diagram techniques are suggested in this work. These new techniques can be used for enhancing the efficiency of existing approaches. One of the main challenges facing design methods is to cope with extraordinarily large state spaces of the system which have to be traversed. During the last years, symbolic methods have attracted great attention in this regard. By means of implicit enumeration, they can achieve significant savings in terms of the computational resources required during the design process.

Symbolic Methods Applied to Formal Verification and Synthesis in Embedded Systems Design