Refine
Document Type
- Report (3)
- Conference Proceeding (2)
- Article (1)
Language
- English (6)
Has Fulltext
- yes (6)
Keywords
- Compiler (1)
- HOL (1)
- bedingte Aktionen (1)
- guarded actions (1)
- synchrone Sprachen (1)
- synchronous languages (1)
Faculty / Organisational entity
There is a well known relationship between alternating automata on finite words and symbolically represented nondeterministic automata on finite words. This relationship is of practical relevance because it allows to combine the advantages of alternating and symbolically represented nondeterministic automata on finite words. However, for infinite words the situation is unclear. Therefore, this work investigates the relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Thereby, we identify classes of alternating omega-automata that are as expressive as safety, liveness and deterministic prefix automata, respectively. Moreover, some very simple symbolic nondeterminisation procedures are developed for the classes corresponding to safety and liveness properties.
This technical report contains the preliminary versions of the regular papers presented at the first workshop on Verification of Adaptive Systems (VerAS) that has been held in Kaiserslautern, Germany, on September 14th, 2007 as part of the 20th International Conference on Theorem Proving in Higher Order Logics. The final versions will be published with Elsevier's Electronic Notes on Theoretical Computer Science (ENTCS). VerAS is the first workshop that aims at considering adaptation as a cross-cutting system aspect that needs to be explicitly addressed in system design and verification. The program committee called for original submissions on formal modeling, specification, verification, and implementation of adaptive systems. There were six submissions from different countries of Europe. Each submission has been reviewed by three programme committee members. Finally, the programme committee decided to accept three of the six submissions. Besides the presentations of the regular papers, the workshop's programme included a tutorial on the `Compositional Verification of Self-Optimizing Mechatronic Systems' held by Holger Giese (University of Paderborn, Germany) as well as three presentations of DASMOD projects on the verification of adaptive systems.
This report gives an overview of the separate translation of synchronous imperative programs to synchronous guarded actions. In particular, we consider problems to be solved for separate compilation that stem from preemption statements and local variable declarations. We explain how we solved these problems and sketch our solutions implemented in the our Averest framework to implement a compiler that allows a separate compilation of imperative synchronous programs with local variables and unrestricted preemption statements. The focus of the report is the big picture of our entire design flow.
This technical report is the Emerging Trends proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), which was held during 10-13 September in Kaiserslautern, Germany. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification.
SHIM is a concurrent deterministic programming language for embedded systems built on rendezvous communication. It abstracts away many details to give the developer a high-level view that includes virtual shared variables, threads as orthogonal statements, and deterministic concurrent exceptions.
In this paper, we present a new way to compile a SHIM-like language into a set of asynchronous guarded actions, a well-established intermediate representation for concurrent systems. By doing so, we build a bridge to many other tools, including hardware synthesis and formal verification. We present our translation in detail, illustrate it through examples, and show how the result can be used by various other tools.
Dataflow process networks (DPNs) are intrinsically data-driven, i.e., node actions are not synchronized among each other and may fire whenever sufficient input operands arrived at a node. While the general model of computation (MoC) of DPNs does not impose further restrictions, many different subclasses of DPNs representing different dataflow MoCs have been considered over time. These classes mainly differ in the kinds of behaviors of the processes. A DPN may be heterogeneous in that different processes in the network belong to different classes of DPNs. A heterogeneous DPN can therefore be effectively used to model and to implement different components of a system with different kinds of processes and, therefore, different dataflow MoCs. This paper presents a model-based design based on different dataflow MoCs including their heterogeneous combinations. In particular, it covers the automatic software synthesis of systems from DPN models. The main objective is to validate, evaluate and compare the artifacts exhibited by different dataflow MoCs at the implementation level of systems under the supervision of a common design tool. Moreover, this work also offers an efficient synthesis method that targets and exploits heterogeneity in DPNs by generating implementations based on the kinds of behaviors of the processes. The proposed synthesis method provides a tool chain including different specialized code generators for specific dataflow MoCs, and a runtime system that finally maps models using a combination of different dataflow MoCs on cross-vendor target hardware.