作者：
K.L. ManFormal Methods Group
Department of Mathematics and Computer Science Eindhovan University of Technology Netherlands
In this paper, we define a formal communication semantics for SystemC/sup FL/ that deals with concurrency and interaction. The communication semantics of SystemC/sup FL/ is formally defined in a standard structured op...
详细信息
In this paper, we define a formal communication semantics for SystemC/sup FL/ that deals with concurrency and interaction. The communication semantics of SystemC/sup FL/ is formally defined in a standard structured operational semantics (SOS) style. The correctness of the proposed communication semantics of SystemC/sup FL/ is also validated. A case study (RPC protocol with refinement) is given to illustrate the use of the newly developed communication semantics of SystemC/sup FL/.
作者：
K.L. ManFormal Methods Group
Department of Mathematics and Computer Science Eindhovan University of Technology Eindhoven Netherlands
SystemC/sup FL/ is a formal language for hardware/software codesign. Principally, SystemC/sup FL/ is the formalization of SyslemC based on classical process algebra ACP. The language is aimed to give formal specificat...
详细信息
SystemC/sup FL/ is a formal language for hardware/software codesign. Principally, SystemC/sup FL/ is the formalization of SyslemC based on classical process algebra ACP. The language is aimed to give formal specification of SystemC designs and perform formal analysis of SystemC processes. This paper, designed for the first-time user of SystemC/sup FL/, guides the reader through modeling, analyzing and verifying designs using SystemC/sup FL/. This paper illustrates the use of SysternC/sup FL/ with two case studies taken from literature.
We consider the distributed implementability problem: Given a labeled transition system TS together with a distribution /spl Delta/ of its actions over a set of processes, does there exist a distributed system over /s...
详细信息
We consider the distributed implementability problem: Given a labeled transition system TS together with a distribution /spl Delta/ of its actions over a set of processes, does there exist a distributed system over /spl Delta/ such that its global transition system is 'equivalent' to TS? We work with the distributed system models of synchronous products of transition systems (Arnold, 1994) and asynchronous automata (Zielonka, 1987). In this paper we provide complexity bounds for the above problem with three interpretations of 'equivalent': as transition system isomorphism, as language equivalence, and as bisimilarity. In particular, we solve problems left open in Castellani et al. (1999) and Morin (1999).
We introduce a family of long-run average properties of Markov chains that are useful for purposes of performance and reliability analysis, and show that these properties can effectively be checked for a subclass of i...
详细信息
We introduce a family of long-run average properties of Markov chains that are useful for purposes of performance and reliability analysis, and show that these properties can effectively be checked for a subclass of infinite-state Markov chains generated by probabilistic programs with recursive procedures. We also show how to predict these properties by analyzing finite prefixes of runs, and present an efficient prediction algorithm for the mentioned subclass of Markov chains.
Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking...
详细信息
Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulated reward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.
This paper presents a formal Petri net-based approach to behaviour modeling for mobile agent systems. Generic agent templates, formalized in Petri net semantics, are proposed to model the components of a distributed m...
详细信息
This special section is devoted to a selection of journal versions of papers that appeared originally in the Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of...
详细信息
This paper presents a model-checking approach for analyzing discrete-time Markov reward models. For this purpose, the temporal logic probabilistic CTL is extended with reward constraints. This allows to formulate comp...
详细信息
Monolithic finite-state probabilistic programs have been abstractly modeled by finite Markov chains, and the algorithmic verification problems for them have been investigated very extensively. In this paper we survey ...
详细信息
作者：
K.L. ManFormal Methods Group
Department of Mathematics and Computer Science Eindhovan University of Technology Eindhoven Netherlands
Based on process algebra, the formal language SystemC/sup FL/ has been developed that is the formalization of SystemC. The language semantics of System C/sup FL/ is formally defined in a standard structured operationa...
详细信息
Based on process algebra, the formal language SystemC/sup FL/ has been developed that is the formalization of SystemC. The language semantics of System C/sup FL/ is formally defined in a standard structured operational semantics (SOS) style.
暂无评论