Search

This paper outlines two approaches|based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines., 18 pages

With cybersecurity increasingly becoming a focus of regulatory concern, both medical device manufacturers and regulators are facing another challenge: how to establish, and also demonstrate, that the devices are also secure. This paper outlines an approach to constructing assurance cases to capture assumptions about the attacker by 1) identifying the hazards of interest to attacker; 2) identifying attack surfaces; 3) enumerating vulnerabilities and attack scenarios; and 4) ranking attack scenarios on the basis of a risk model. Introducing the security considerations early in the design cycle, we can better integrate security with existing engineering processes to yield documents that both improve the engineering processes and are acceptable for regulatory oversight.

Formal methods and testing are two important approaches that assist in the development of high quality software. While traditionally these approaches have been seen as rivals, in recent years a new consensus has developed in which they are seen as complementary. This article reviews the state of the art regarding ways in which the presence of a formal specification can be used to assist testing.

We revisit the question of the uniqueness of solutions to fixpoint equations modulo observation congruence. In the literature various sufficient conditions are given for the uniqueness of such solutions for a given signature of process combinators, such as guardedness and sequentiality (CCS) or the absence of abstraction (ACP), concealment (CSP), or hiding (LOTOS) combinators. Our study is based on contexts, i.e. behaviour expressions with ‘holes’, whose operational semantics can be characterised by action transductions. Using these we define the context properties of opacity and abstraction-freedom, thus generalising the signature dependent conditions, which can be deduced from these properties. The condition of abstraction-freedom is further improved upon in two ways. First, by relativizing the notion of abstraction-freedom to essential guarding actions, allowing proofs of uniqueness in more cases. Second, by a new criterion based on context transductions that can be applied even more generally. We apply it to a fix-point equation based on a context where a hiding combinator removes what seem to be essential guarding actions. This implies that the condition of (relativised) abstraction-freedom is generally too strict.

In earlier work, we presented a process algebra, PACSR, that uses a notion of resource failure to capture probabilistic behavior in reactive systems. PACSR also supports an operator for resource hiding. In this paper, we carefully consider the interaction between these two features from an axiomatic perspective. For this purpose, we introduce a subset of PACSR, called "PACSR-lite", that allows us to isolate the semantic issues surrounding resource hiding in a probabilistic setting, and provide a sound and complete axiomatization of strong bisimulation for this fragment. © 2001 Elsevier Science B.V. All rights reserved. 80 1 3 13

PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilistic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parameterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also given. Finally, PACSR and the logic are illustrated with a telecommunications example. © 1998, Springer Verlag. All rights reserved. 1466 389 404 Sponsors: Conference code: 143949 Cited By :10

We compare propositional temporal logics by comparing the equivalences that they induce on models. Linear time, branching time and partial order temporal logics are considered. The logics are interpreted on occurrence transition systems, generated by labelled prime event structures without autoconcurrency. The induced equivalences are also compared to directly defined equivalences, e.g., history preserving bisimulation, pomset bisimulation, pomset trace equivalence, and others. It is then shown which of the induced equivalences are and which are not preserved under action refinement.

Suppose one has a system that has a synchronous interface with its environment. Now, suppose that one refines this system and changes its interface to an asynchronous one. Whatever is meant here by refinement, it cannot be standard (process) refinement since the interface actions have changed; nor is it action refinement in the sense that a process is substituted for an action, as the intention presumably is to allow the system to proceed without having to wait until the environment is willing to synchronize. In this paper we propose a notion of interface refinement of which changing synchronous to asynchronous communication is an instance; as is in fact the reverse change. This notion of interface refinement is quite powerful; it generalizes all existing methods w.r.t. the class of interface changes that it allows. The major part of the paper is concerned with developing proof rules with which to verify interface refinement. We use (linear) temporal logic as specification language and an adaptation of the Manna-Pnueli verification framework. The method is illustrated by verifying an interface change in which synchronous communication is replaced by asynchronous send and receive. Proofs of the various theorems and lemma's are delegated to an appendix.

This paper is concerned with finding complete axiomatizations of probabilistic processes. We examine this problem within the context of the process algebra ACP and obtain as our end-result the axiom system prACP I −- , a probabilistic version of ACP which can be used to reason algebraically about the reliability and performance of concurrent systems. Our goal was to introduce probability into ACP in as simple a fashion as possible. Optimally, ACP should be the homomorphic image of the probabilistic version in which the probabilities are forgotten.