Hidden communication systems (HCS) embed covert messages within ordinary network activity to hide the presence of communication. In practice, the undetectability of an HCS is typically evaluated using ad hoc traffic statistics or specific detectors, making security claims tightly coupled to experimental setups and implicit adversarial assumptions. In this work, we formalize undetectability as the statistical indistinguishability of observable execution traces under two deployments: a baseline system without hidden communication and an HCS deployment carrying covert traffic. Undetectability is expressed as a bound on a quantitative measure of distance between the trace distributions induced by these two executions. We develop Maude-HCS, an executable modeling and analysis framework that provides a principled and executable foundation for reasoning about undetectability-performance tradeoffs in complex HCS designs. Maude-HCS allows designers to specify protocol behavior, adversary observables, and environmental assumptions, and to generate Monte Carlo samples from the induced trace distributions. We demonstrate that Maude-HCS can be used to audit claims of undetectability by estimating the true and false positive rates of a statistical test and converting these estimates into lower bounds on undetectability measures such as KL divergence. This enables systematic evaluation of detectability and its tradeoffs with performance under explicitly stated modeling assumptions. Finally, we evaluate Maude-HCS on proof-of-concept tunneling-based HCS instantiations and validate model predictions against measurements from a physical testbed. For passive adversaries observing timing and traffic statistics, we quantify how undetectability and performance vary with protocol configuration, background traffic, and network loss, and demonstrate strong semantic alignment between model-based guarantees and empirical results.

The Border Gateway Protocol (BGP) is employed by autonomous systems (ASes), such as network operators or ISPs, to build routing tables. However, depending on the routing policies implemented by these ASes, BGP may fail to converge, potentially rendering the network inoperative. This paper introduces a workflow that leverages SMT solvers and rewriting tools to automate the verification of BGP convergence within a given AS network. We encode the convergence conditions defined by the Metarouting theoretical framework as an SMT problem. While SMT solvers can automatically determine whether BGP will converge, they do not generate counterexample traces in cases of divergence. To overcome this shortcoming, we propose a sound divergence criterion. We also construct an executable model for verifying BGP convergence, which can be automated using the Maude rewriting tool to produce witness traces in divergent scenarios. The effectiveness of our approach is demonstrated through a series of experiments.

Maude is a high-performance logical framework based on rewriting logic and supporting formal specification, verification and declarative programming of concurrent systems. Since most concurrent open systems are made up of actor-like objects that communicate with each other through message passing, Maude provides special features to support their specification, verification and programming. Since open systems are heterogeneous, involving widely different kinds of objects such as sensors, actuators, devices, databases, graphical user interfaces, and so on, Maude supports declarative message-passing interaction between Maude objects and a wide variety of heterogeneous external objects. In this paper we explain and illustrate a methodology where an open system can first be designed and verified in Maude and then implemented as a distributed system of heterogeneous objects in a way that seamlessly bridges the gap between its formal specification and verification and its distributed implementation.

Abstract Rewriting Modulo SMT combines two powerful automated deduction techniques (1) rewriting and (2) SMT-solving. Rewriting enables the specification of behavior of systems using rewriting rules, while SMT theories specify system properties. Rewriting Modulo SMT is enabled by combining existing tools, such as Maude and SMT solvers. Search algorithms used for carrying out Rewriting Modulo SMT, however, cannot exploit the incremental solving features available in SMT solvers as they are based on breadth-first search. This paper addresses this limitation by proposing Incremental Rewriting Modulo SMT Theories, which is a syntactical restriction to rewriting rules. This restriction turns out to naturally be used in several applications of Rewriting Modulo SMT, including the verification of algorithms, cyber-physical systems, and security protocols. Moreover, we propose a Hybrid-Search algorithm for Incremental Rewriting Modulo SMT Theories that combines breadth-first search and depth-first search, thus enabling incremental SMT-solving. We demonstrate through a collection of existing benchmarks that the Hybrid-Search algorithm can achieve a 10 times performance improvement in verification times.

Composition is an important feature of a specification language, as it enables the design of a complex system in terms of a product of its parts. Decomposition is equally important in order to reason about structural properties of a system. Usually, however, a system can be decomposed in more than one way, each optimizing for a different set of criteria. We extend an algebraic component-based model for cyber-physical systems to reason about decomposition. In this model, components compose using a family of algebraic products, and decompose, under some conditions, given a corresponding family of division operators. We use division to specify invariant of a system of components, and to model desirable updates. We apply our framework to design a cyber-physical system consisting of robots moving on a shared field, and identify desirable updates using our division operator.

We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component composition. These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors. Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behavior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.

Abstract Given the complexity of cyber-physical systems (CPS), such as swarms of drones, often deviations, from a planned mission or protocol, occur which may in some cases lead to harm and losses. To increase the robustness of such systems, it is necessary to detect when deviations happen and diagnose the cause(s) for a deviation. We build on our previous work on soft agents, a formal framework based on using rewriting logic for specifying and reasoning about distributed CPS, to develop methods for diagnosis of CPS at design time. We accomplish this by (1) extending the soft agents framework with Fault Models; (2) proposing a protocol specification language and the definition of protocol deviations; and (3) development of workflows/algorithms for detection and diagnosis of protocol deviations. Our approach is partially inspired by existing work using counterfactual reasoning for fault ascription. We demonstrate our machinery with a collection of experiments.

Development of automated technological systems has seen the increase in interconnectivity among its components. This includes Internet of Things (IoT) and Industry 4.0 (I4.0) and the underlying communication between sensors and controllers. This paper is a step toward a formal framework for specifying such systems and analyzing underlying properties including safety and security. We introduce automata systems (AS) motivated by I4.0 applications. We identify various subclasses of AS that reflect different types of requirements on I4.0. We investigate the complexity of the problem of functional correctness of these systems as well as their vulnerability to attacks. We model the presence of various levels of threats to the system by proposing a range of intruder models, based on the number of actions intruders can use.

Protocol security verification is one of the best success stories of formal methods. However, some aspects important to protocol security, such as time and resources, are not covered by many formal models. While timing issues involve e.g., network delays and timeouts, resources such as memory, processing power, or network bandwidth are at the root of Denial of Service (DoS) attacks which have been a serious security concern. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable not only to powerful intruders, but also to resource-bounded intruders that cannot generate or intercept arbitrarily large volumes of traffic. A refined Dolev–Yao intruder model is proposed, that can only consume at most some specified amount of resources in any given time window. Timed protocol theories that specify service resource usage during protocol execution are also proposed. It is shown that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Additionally, we describe a decidable fragment in the verification of the leakage problem for resource-sensitive timed protocol theories.

Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.

Without appropriate counter-measures, cyber-attacks can exploit the increased system connectivity provided by Industry 4.0 (I4.0) to cause catastrophic events, by, e.g., injecting or tampering with messages. The solution supported by standards, such as, OPC-UA, is to sign or encrypt messages. However, given the limited resources of devices, instead of encrypting all messages in the network, it is better to encrypt only the messages that if tampered with or injected, could lead to undesired configurations. This paper describes the use of formal verification to analyse the security of I4.0 applications. We formalize in Rewriting Logic, I4.0 applications and systems, i.e., networked sets of devices, and a symbolic intruder model. Our formalization can be executed by the tool Maude to automate such security analysis, e.g., determine which messages are sufficient to sign in order avoid injection and tampering attacks.

Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between tw o agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with an attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.

Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.

We present ADDSEN middleware as a holistic solution for Adaptive Data processing and dissemination for Drone swarms in urban SENsing. To efficiently process sensed data in the middleware, we have proposed a cyber-physical sensing framework using partially ordered knowledge sharing for distributed knowledge management in drone swarms. A reinforcement learning dissemination strategy is implemented in the framework. ADDSEN uses online learning techniques to adaptively balance the broadcast rate and knowledge loss rate periodically. The learned broadcast rate is adapted by executing state transitions during the process of online learning. A strategy function guides state transitions, incorporating a set of variables to reflect changes in link status. In addition, we design a cooperative dissemination method for the task of balancing storage and energy allocation in drone swarms. We implemented ADDSEN in our cyber-physical sensing framework, and evaluation results show that it can achieve both maximal adaptive data processing and dissemination performance, presenting better results than other commonly used dissemination protocols such as periodic, uniform and neighbor protocols in both single-swarm and multi-swarm cases.

The core of the Pathway Logic signal transduction model (STM) is a theory in the rewriting logic language Maude. This theory provides a language for representing the signaling state of a cell and its components, and rewrite rules representing possible signaling events. Used as a theory in rewriting logic, statements about signal propagation can be proved. The theory can also be viewed as a database that can be queried, for example, to find the events in which a given protein might participate or to retrieve all signaling events (rules) of a given type. Given a representation of a cell state, an executable model can be derived from the theory. This model can be executed to observe a possible behavior, or model checked to study properties of signal propagation pathways. Finally, the theory can be viewed as term in the meta-theory. Using reflection, the theory can be mapped to terms in other formalisms, to access additional reasoning tools; to annotated graphical representations for visualization; or to an external representation such as JSON, SBML or BIOPAX for sharing with other formal systems. The talk will begin with a perspective on formal modeling. We will then discuss identification and representation of elements of a theory of signal transduction motivated by experimental evidence. Finally we show how the views of the resulting theory are used in practice and how the ideas generalize to modeling other cellular processes such as glycosylation and immune system.

Formal executable models provide a means to gain insights into the behavior of complex distributed systems. Ideas can be prototyped and assurance gained by carrying out analyses at different levels of fidelity: searching for desirable or undesirable behaviors, determining effects of perturbing the system, and eventually investing effort to carry out formal proofs of key properties. This modeling approach applies to a wide range of systems, including a variety of protocols and networked cyber-physical systems. It is also emerging as an important tool in understanding many different aspects of biological systems. Rewriting logic (RWL) is a formalism that is well-suited to developing and working with formal executable models. In RWL term rewriting is used to represent both structure (equational properties and functions) and transformation / behavior. Logics and inference systems can be naturally represented in RWL, as can the structure and behavior of distributed systems both engineered and natural. Maude is a high performance realization of Rewriting Logic. Maude specifications are naturally executable and the Maude environment provides a variety analysis tools to reason about properties of models. These include reachability analysis, symbolic execution (narrowing), and model-checking. In addition, Maude is reflective. This provides a powerful mechanism for extension. The talk will present a sampling of executable specifications using Maude and its extensions.

The Border Gateway Protocol (BGP) is the single inter-domain routing protocol that enables network operators within each autonomous system (AS) to influence routing decisions by independently setting local policies on route filtering and selection. This independence leads to fragile networking and makes analysis of policy configurations very complex. To aid the systematic and efficient study of the policy configuration space, this paper presents network reduction, a scalability technique for policy-based routing systems. In network reduction, we provide two types of reduction rules that transform policy configurations by merging duplicate and complementary router configurations to simplify analysis. We show that the reductions are sound, dual of each other and are locally complete. The reductions are also computationally attractive, requiring only local configuration information and modification. We have developed a prototype of network reduction and demonstrated that it is applicable on various BGP systems and enables significant savings in analysis time. In addition to making possible safety analysis on large networks that would otherwise not complete within reasonable time, network reduction is also a useful tool for discovering possible redundancies in BGP systems.

BACKGROUND: As more complete genome sequences become available, bioinformatics challenges arise in how to exploit genome sequences to make phenotypic predictions. One type of phenotypic prediction is to determine sets of compounds that will support the growth of a bacterium from the metabolic network inferred from the genome sequence of that organism. RESULTS: We present a method for computationally determining alternative growth media for an organism based on its metabolic network and transporter complement. Our method predicted 787 alternative anaerobic minimal nutrient sets for Escherichia coli K-12 MG1655 from the EcoCyc database. The program automatically partitioned the nutrients within these sets into 21 equivalence classes, most of which correspond to compounds serving as sources of carbon, nitrogen, phosphorous, and sulfur, or combinations of these essential elements. The nutrient sets were predicted with 72.5% accuracy as evaluated by comparison with 91 growth experiments. Novel aspects of our approach include (a) exhaustive consideration of all combinations of nutrients rather than assuming that all element sources can substitute for one another(an assumption that can be invalid in general) (b) leveraging the notion of a machinery-duplicating constraint, namely, that all intermediate metabolites used in active reactions must be produced in increasing concentrations to prevent successive dilution from cell division, (c) the use of Satisfiability Modulo Theory solvers rather than Linear Programming solvers, because our approach cannot be formulated as linear programming, (d) the use of Binary Decision Diagrams to produce an efficient implementation. CONCLUSIONS: Our method for generating minimal nutrient sets from the metabolic network and transporters of an organism combines linear constraint solving with binary decision diagrams to efficiently produce solution sets to provided growth problems.

The BGP (Border Gateway Protocol) is the single inter-domain routing protocol that enables network operators within each autonomous system (AS) to influence routing decisions by independently setting local policies on route filtering and selection. This independence leads to fragile networking and makes analysis of policy configurations very complex. To aid the systematic and efficient study of the policy configuration space, this paper presents a reduction calculus on policy-based routing systems. In the calculus, we provide two types of reduction rules that transform policy configurations by merging duplicate and complementary router configurations to simplify analysis. We show that the reductions are sound, dual of each other and are locally complete. The reductions are also computationally attractive, requiring only local configuration information and modification. These properties establish our reduction calculus as a sound, efficient, and complete theory for scaling up existing analysis techniques.

Activities such as clinical investigations or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols, and activities can form the foundation for automated assistants to aid planning, monitoring, and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, that is, they may have different outcomes whenever applied. We demonstrate how specifications in our model can be straightforwardly mapped to the rewriting logic language Maude, and how one can use existing techniques to improve performance. Finally, we also determine the complexity of the plan compliance problem, that is, finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, that is, their pre and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects.

Today's inter-domain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfiguration by individual autonomous systems (ASes). Existing configuration analysis techniques are either manual and tedious, or do not scale beyond a small number of nodes due to the state explosion problem. To aid the diagnosis of misconfigurations in real-world large BGP systems, this paper presents BGPVerif , a reduction based analysis toolkit. The key idea is to reduce BGP system size prior to analysis while preserving crucial correctness properties. BGPVerif consists of two components, NetReducer that simplifies BGP configurations, and NetAnalyzer that automatically detects routing oscillation. BGPVerif accepts a wide range of BGP configuration inputs ranging from real-world traces (Rocketfuel network topologies), randomly generated BGP networks (GT-ITM), Cisco configuration guidelines, as well as arbitrary user-defined networks. BGPVerif illustrates the applicability, efficiency, and benefits of the reduction technique, it also introduces an infrastructure that enables networking researchers to interact with advanced formal method tool.

Resource-limited mobile embedded systems can benefit greatly from dynamic adaptation of system parameters. We propose a novel approach that employs iterative tuning using lightweight formal verification at runtime with feedback for dynamic adaptation. One objective of this approach is to enable trade-off analysis across multiple layers (e.g., application, middleware, OS) and predict the possible property violations as the system evolves dynamically over time. Specifically, an executable formal specification is developed for each layer of the mobile system under consideration. The formal specification is then analyzed using statistical property checking and statistical quantitative analysis, to determine the impact of various resource management policies for achieving desired timing/QoS properties. Integration of formal analysis with dynamic behavior from system execution results in a feedback loop that enables model refinement and further optimization of policies and parameters. We demonstrate the applicability of this approach to the adaptive provisioning of resource-limited distributed real-time systems using a mobile multimedia case study.

Interdomain routing stitches the disparate parts of the Internet together, making protocol stability a critical issue to both researchers and practitioners. Yet, researchers create safety proofs and counterexamples by hand and build simulators and prototypes to explore protocol dynamics. Similarly, network operators analyze their router configurations manually or using homegrown tools. In this paper, we present a comprehensive toolkit for analyzing and implementing routing policies, ranging from high-level guidelines to specific router configurations. Our Formally Safe Routing (FSR) toolkit performs all of these functions from the same algebraic representation of routing policy. We show that routing algebra has a natural translation to both integer constraints (to perform safety analysis with SMT solvers) and declarative programs (to generate distributed implementations). Our extensive experiments with realistic topologies and policies show how FSR can detect problems in an autonomous system's (AS's) iBGP configuration, prove sufficient conditions for Border Gateway Protocol (BGP) safety, and empirically evaluate convergence time.

This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.

Adaptive resource management is critical to ensuring the quality of real-time distributed applications, particularly for energy-constrained mobile handheld devices. In this context, an optimization that simultaneously considers multiple layers (e.g., application, middleware, operating system) needs to be developed for continuous adaptation of system parameters. The tuning of system parameters greatly affects the system's ability to meet QoS requirements, and also directly affects the energy consumption and system robustness. We present a novel approach to developing cross-layer optimization for resource limited real-time distributed systems, based on a constraint refinement technique combined with formal specification and feedback from system implementation. Our approach tunes the parameters in a compositional manner allowing coordinated interaction among sub-layer optimizers that enables holistic cross-layer optimization. We present experiments on a realistic multimedia application which demonstrate that constraint refinement enables us to generate robust and near optimal parameter settings. The constraint language can be used as an interface for composition by encapsulating the details of local optimization algorithms.

This paper presents a study of possible extensions of pathway logic to represent and reason about semiquantitative and probabilistic aspects of biological processes. The underlying theme is the annotation of reaction rules with affinity information that can be used in different simulation strategies. Several such strategies were implemented, and experiments carried out to test feasibility, and to compare results of different approaches. Dimerization in the ErbB signalling network, important in cancer biology, was used as a test case.

Many dynamical processes can be represented as directed attributed graphs or Petri nets where relationships between various entities are explicitly expressed. Signaling networks modeled as Petri nets are one class of such graphical modeling and representations. These networks encode how different protein in specific compartments, interact to create new protein products. Initially, the proteins and rules governing their interactions are curated from literature and then refined with experimental data. Variation in these networks occurs in topological structure, size, and weights associated on edges. Collectively, these variations are quite significant for manual and interactive analysis. Furthermore, as new information is added to these networks, the emergence of new computational models becomes paramount. From this perspective, hierarchical spectral methods are proposed and applied for inferring similarities and dissimilarities from an ensemble of graphs that corresponds to reaction networks. The technique has been implemented and tested on curated signaling networks that are derived for breast cancer cell lines

We have discussed key features of intra-cellular signaling processes as computational primitives and shown how they can be modeled, executed and analyzed using pathway logic. This is intended to lay the ground for deeper formal studies of the relations between the building blocks and composition mechanisms of biological processes and foundations of computing. Pathway logic has a knowledge base of over 1000 rules and 600 basic components and is used to analyze signaling in different cell types. Questions of interest include effects of perturbations (knockouts, knockins) and finding upstream and downstream effects of given components.

We extend an executable specification of a state-of-the-art secure group communication subsystem to explore two dimensions of adaptability, namely security and synchrony under crash-recovery and intermittent connectivity scenarios. In particular, we relax the traditional requirement of virtual synchrony and propose various generic optimizations, while preserving essential security guarantees. In order to evaluate how practical and effective our generic optimizations are, we integrate the specification into ns2, bridging the gap between formal specification and classical network simulation

We propose a formal model for reputation-based trust management. In contrast to credential-based trust management, in our framework an agent's reputation serves as the basis for trust. For example, an access control policy may consider the agent's re

Systems that provide distributed multimedia services are subject to constant evolution; customizable middleware is required to effectively manage this change. Middleware services for resource management execute concurrently with each other, and with application activities, and can, therefore, potentially interfere with each other. To ensure cost-effective QoS in distributed multimedia systems, safe composability of resource management services is essential. In this article, we present a meta-architectural framework, the Two-Level Actor Model (TLAM) for customizable QoS-based middleware, based on the actor model of concurrent active objects. Using TLAM, a semantic model for specifying and reasoning about components of open distributed systems, we show how a QoS brokerage service can be used to coordinate multimedia resource management services in a safe, flexible, and efficient manner. In particular, we show a system in which the multimedia actor behaviors satisfy the specified requirements and provide the required multimedia service. The behavior specification leaves open the possibility of a variety of algorithms for resource management. Furthermore, constraints are identified that are sufficient to guarantee noninterference among the multiple broker resource management services, as well as providing guidelines for the safe composition of additional services.

We present a set-based control flow analysis for an imperative, concurrent object calculus extending the Fisher-Honsell-Mitchell functional object-oriented calculus described in Fisher, Honsell and Mitchell, (1993). The analysis is shown to be sound with respect to a transition-system semantics.

We present an actor language which is an extension of a simple functional language, and provide an operational semantics for this extension. Actor configurations represent open distributed systems, by which we mean that the specification of an actor system explicitly takes into account the interface with external components. We study the composability of such systems. We define and study various notions of testing equivalence on actor expressions and configurations. The model we develop provides fairness. An important result is that the three forms of equivalence, namely, convex, must, and may equivalences, collapse to two in the presence of fairness. We further develop methods for proving laws of equivalence and provide example proofs to illustrate our methodology.

This paper builds domain theoretic concepts upon an operational foundation. The basic operational theory consists of a single step reduction system from which an operational ordering and equivalence on programs are defined. The theory is then extended to include concepts from domain theory, including the notions of directed set, least upper bound, complete partial order, monotonicity, continuity, finite element, ω -algebraicity, full abstraction, and least fixed point properties. We conclude by using these concepts to construct a (strongly) fully abstract continuous model for our language. In addition we generalize a result of Milner and prove the uniqueness of such models.

this paper we consider remote creation, migration, and reachability snapshot services: their specification at different levels of abstraction, and their composition. 1.1 About Actors

In this paper we introduce a variable typed logic of effects inspired by the variable type systems of Feferman for purely functional languages. VTLoE (Variable Typed Logic of Effects) is introduced in two stages. The first stage is the first-order theory of individuals built on assertions of equality (operational equivalence à la Plotkin), and contextual assertions. The second stage extends the logic to include classes and class membership. The logic we present provides an expressive language for defining and studying properties of programs including program equivalences, in a uniform framework. The logic combines the features and benefits of equational calculi as well as program and specification logics. In addition to the usual first-order formula constructions, we add contextual assertions. Contextual assertions generalize Hoare′s triples in that they can be nested, they can be used as assumptions, and their free variables can be quantified. They are similar in spirit to program modalities in dynamic logic. We use the logic to establish the validity of the Meyer Sieber examples in an operational setting. The theory allows for the construction of inductively defined sets and derivation of the corresponding induction principles. We hope that classes may serve as a starting point for studying semantic notions of type. Naive attempts to represent ML types as classes fail in the sense that ML inference rules are not valid.

A.R. Meyer and K. Sieber (Proc. 15th ACM. Symp. on Principles of Programming Languages, 1988, p.191-208) gave a series of examples of programs that are operationally equivalent (according to the intended semantics of block-structured Algol-like programs) but are not given equivalent denotations in traditional denotational semantics. They propose various modifications to the denotational semantics that solve some of these discrepancies, but not all. The present authors approach the same problem, but from an operational rather than a denotational perspective. They present the first-order part of a new logic for reasoning about programs, and they use this logic to prove the equivalence of the Meyer-Sieber examples.>

In this paper we report progress in the development of methods for reasoning about the equivalence of objects with memory, and the use of these methods to describe sound operations on objects in terms of formal program transformations. We also formalize three different aspects of objects: their specification, their behavior, and their canonical representation. Formal connections among these aspects provide methods for optimization and reasoning about systems of objects. To illustrate these ideas we give a formal derivation of an optimized specialized window editor from generic specifications of its components. A new result in this paper enables one to make use of symbolic evaluation (with respect to a set of constraints) to establish the equivalence of objects. This form of evaluation is not only mechanizable, it is also generalizes the conditions under which partial evaluation usually takes place. 1 Overview In [19] a general challenge for partial evaluation technology was presented ...

Abstract Traditionally the view has been that direct expression of control and store mechanisms and clear mathematical semantics are incompatible requirements. This paper shows that adding objects with memory to the call-by-value lambda calculus results in a language with a rich equational theory, satisfying many of the usual laws. Combined with other recent work, this provides evidence that expressive, mathematically clean programming languages are indeed possible.

The authors present a formal system for deriving assertions about programs with side effects. The assertions considered are the following: (i) the expression e diverges (i.e. fails to reduce to a value); and (ii) e/sub 0/ and e/sub 1/ are strongly isomorphic (i.e. reduce to the same value and have the same effect on memory up to production of garbage). The e, e/sub j/ are expressions of a first-order scheme- or Lisp-like language with the data operations atom, eq, car, cdr, cons, setcar, setcdr, the control primitives let and if, and recursive definition of function symbols.>