Sciweavers

ACSD
2001
IEEE
134views Hardware» more  ACSD 2001»
14 years 2 months ago
Embedding Imperative Synchronous Languages in Interactive Theorem Provers
We present a new way to define the semantics of imperative synchronous languages by means of separating the control and the data flow. The control flow is defined by predicates th...
Klaus Schneider
ACSD
2001
IEEE
91views Hardware» more  ACSD 2001»
14 years 2 months ago
Synthesis of Net Systems with Inhibitor Arcs from Step Transition Systems
We here consider transition systems of Elementary Net Systems with Inhibitor Arcs. There are basically two di erent types of non-interleaving semantics of such Petri nets, the a-po...
Marta Pietkiewicz-Koutny
ACSD
2001
IEEE
121views Hardware» more  ACSD 2001»
14 years 2 months ago
A structural encoding technique for the synthesis of asynchronous circuits
This paper presents a method for the automatic synthesis of asynchronous circuits from Petri net specifications. The method is based on a structural encoding of the system in such ...
Josep Carmona, Jordi Cortadella, Enric Pastor
ACSD
2001
IEEE
83views Hardware» more  ACSD 2001»
14 years 2 months ago
Overcoming Heterophobia: Modeling Concurrency in Heterogeneous Systems
We describe a framework where formal models can be rigorously defined and compared, and their interconnections can be unambiguously specified. We use trace algebra and trace struc...
Jerry R. Burch, Roberto Passerone, Alberto L. Sang...
ACSD
2001
IEEE
102views Hardware» more  ACSD 2001»
14 years 2 months ago
Exploration Testing
This paper describes a new way of testing reactive systems as investigated by the RATE-project at the Tampere University of Technology. We abandon the idea of systematically using...
Juhana Helovuo, Sari Leppänen
ACSD
2001
IEEE
74views Hardware» more  ACSD 2001»
14 years 2 months ago
From Code to Models
One of the corner stones of formal methods is the notion traction enables analysis. By the construction of act model we can trade implementation detail for analytical power. The i...
Gerard J. Holzmann
ACSD
2001
IEEE
118views Hardware» more  ACSD 2001»
14 years 2 months ago
Correct Performance of Transaction Capabilities
The correctness of an optimisation of the Transport Capabilities Application Part of the Signalling System No. 7 is formalised as a branching bisimulation which is relaxed to allo...
Thomas Arts, Izak van Langevelde
ACSD
2001
IEEE
112views Hardware» more  ACSD 2001»
14 years 2 months ago
Software Implementation of Synchronous Programs
Synchronous languages allow a high level, concurrent, and deterministic description the behavior of reactive systems. Thus, they can be used advantageously for the programming of ...
Charles Andre, Frédéric Boulanger, A...