We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is combined with inductive theorem proving to discharge inductive verification conditions that ensure useful symbolic state space reductions. An obvious combination is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible combination. In this paper we focus instead on a new deductive model checking methodology to verify invariants —including inductive invariants— of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle . Inductive verification conditions not discharged automatically by the oracle are dealt with by commands that refine some constrained patterns by useful semantic equivalences, and by using an inductive theorem prover in interactive mode. This methodology is demonstrated by means of concurrent system examples using two Maude tools working in tandem: the DM-Check narrowing-based symbolic model checker, and the NuITP inductive theorem prover.

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.

Abstract Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.

Formalizing languages with binders (such as programming languages and logics) within a logical framework with zero representational distance (i.e., the calculus and its representation look the same) poses non-trivial challenges, including: faithful representation of syntax and binding operators; support for calculus-specific equivalences; faithful representation of the language dynamics (operational semantics); and generation of correct-by-construction implementations. We show how rewriting logic can meet these challenges. More precisely, we show how a general notion of binder signature can be axiomatized in rewriting logic and we propose a general methodology to specify languages with binders, including their structural congruences and operational semantics. We also show how rewriting logic methods provide executable specifications of languages with binders. We use the π -calculus as a running example because it illustrates well the above-mentioned challenges.

NuITP is an inductive equational theorem prover that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms) to verify equational programs with expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms in Maude and in other equational languages. The present paper introduces the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark.

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.

Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-deterministic local transformations on the state. Sometimes a controlled application of these rules is required to reduce non-determinism, to capture global, goal-oriented or efficiency concerns, or to select specific executions for their analysis. That is what we call a strategy. In order to express them, respecting the separation of concerns principle, a Maude strategy language was proposed and developed. The first implementation of the strategy language was done in Maude itself using its reflective features. After ample experimentation, some more features have been added and, for greater efficiency, the strategy language has been implemented in C++ as an integral part of the Maude system. This paper describes the Maude strategy language along with its semantics, its implementation decisions, and several application examples from various fields.

Today’s distributed systems must satisfy bothqualitativeandquantitativeproperties. These properties are analyzed using very different formal frameworks: expressive untimed and non-probabilistic frameworks, such as TLA+ and Hoare/separation logics, for qualitative properties; and timed/probabilistic-automaton-based ones, such as Uppaal and Prism, for quantitative ones. This requires developing two quite different models of the same system, without guarantees of semantic consistency between them. Furthermore, it is very hard or impossible torepresentintrinsic features of distributed object systems—such as unbounded data structures, dynamic object creation, and an unbounded number of messages—using finite automata. In this paper we bridge this semantic gap, overcome the problem of manually having to develop two different models of a system, and solve the representation problem by: (i) defining a transformation from a very general class of distributed systems (a generalization of Agha’s actor model) that maps an untimed non-probabilistic distributed system model suitable for qualitative analysis to a probabilistic timed model suitable for quantitative analysis; and (ii) proving the two models semantically consistent. We formalize our models in rewriting logic, and can therefore use the Maude tool to analyze qualitative properties, and statistical model checking with PVeStA to analyze quantitative properties. We have automated this transformation and integrated it, together with the PVeStA statistical model checker, into theActors2PMaudetool. We illustrate the expressiveness of our framework and our tool’s ease of use by automatically transforming untimed, qualitative models of numerous distributed system designs—including an industrial data store and a state-of-the-art transaction system—into quantitative models to analyze and compare the performance of different designs.

The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of different, increasingly efficient formulations of the homeomorphic embedding relation modulo axioms that we implement in Maude. Our experimental results show that the most efficient version indeed pays off in practice.

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

Abstract Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) (either all or none of a transaction’s updates are visible to other transactions) and prevention of lost updates (PLU). Existing distributed transaction systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency ), but this comes at the price of lower performance. In this paper we propose a new distributed transaction protocol, ROLA, that targets application scenarios where only RA and PLU are needed. We formally specify ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) perform statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by also modeling and analyzing in Maude the well-known protocols Walter and Jessy that also guarantee RA and PLU. Our statistical model checking results show that ROLA outperforms both Walter and Jessy.

Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency ), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness , we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.

We perform an automated analysis of two devices developed by Yubico: YubiKey, de- signed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol an- alyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known at- tacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Reachability logic has been applied to 𝕂 rewrite-rule-based language definitions as a language-generic logic of programs to verify a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but also rewrite-theory-ge neric, so that we can verify both conventional programs based on their rewriting logic operational semantics and distributed system designs specified as rewrite theories. A theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Particular attention is given to increasing the logic’s automation by means of constructor-based semantic unification, matching, narrowing, and satisfiability procedures. The relationships to Hoare logic and LTL are discussed, new methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new methods are presented.

Abstract A pattern t , i.e., a term possibly with variables, denotes the set (language) 〚 t 〛 of all its ground instances . In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. But for the more expressive patterns needed in declarative languages supporting rich type disciplines such as subtype polymorphism, untyped pattern operations and algorithms break down. We show how they can be properly defined by means of a signature transformation Σ ↦ Σ # that enriches the types of Σ . We also show that this transformation allows a systematic reduction of the first-order logic properties of an initial order-sorted algebra supporting subtype-polymorphic functions to equivalent properties of an initial many-sorted (i.e., simply typed) algebra. This yields a new, simple proof of the known decidability of the first-order theory of an initial order-sorted algebra.

Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool.

A declarative program P is a theory in a given computational logic L, so that computation with such a program is efficiently implemented as deduction in L. That is why inference systems are crucial: they both (i) define the logical semantics of a language in its underlying logic L, and (ii) specify the execution of programs in a correct implementation. The notion of operational termination (OT) of a declarative program P identifies termination with absence of infinite inference with P. We further develop the OT notion for declarative programs in general logics with schematic inference systems and characterize OT in terms of chains of proof jumps. We also generalize the Dependency Pair Framework for Term Rewriting Systems to an arbitrary schematic logic L, so that methods for proving declarative programs OT become available for a very wide range of declarative languages. We illustrate the usefulness of the general OT methods we propose by three case studies in three logics: that of Conditional Term Rewriting Systems, the Typed λ-calculus, and Membership Rewriting Logic. In particular, we show how various programs that could not be proved terminating with existing methods can be proved OT with the methods presented here.

Recent advances in the automated analysis of cryptographic protocols have aroused new interest in the practical application of unification modulo theories, especially theories that describe the algebraic properties of cryptosystems. However, this application requires unification algorithms that can be easily implemented and easily extended to combinations of different theories of interest. In practice this has meant that most tools use a version of a technique known as variant unification. This requires, among other things, that the theory be decomposable into a set of axioms B and a set of rewrite rules R such that R has the finite variant property with respect to B. Most theories that arise in cryptographic protocols have decompositions suitable for variant unification, but there is one major exception: the theory that describes encryption that is homomorphic over an Abelian group.

Security-as-a-Service (SecaaS) is gaining popularity, with cloud-based anti-spam and anti-virus leading the way. In this work we look at key management as a security service and focus on group key management witha central group key manager. Specifically, we analyze are writing logic model of a ZooKeeper-based group key management service specified in Maude and study its tolerance to faults and performance as it scales to service larger groups using the PVeStA statistical model checking tool.

A concurrent system can be naturally specified as a rewrite theory R = (Sigma, E, R) where states are elements of the initial algebra of terms modulo E and concurrent transitions are axiomatized by the rewrite rules R. Under simple conditions, narrowing with rules R modulo equations E can be used to symbolically represent the system's state space by means of terms with logical variables. We call this symbolic representation a "logical state space" and it can also be used for model checking verification of LTL properties. Since in general such a logical state space can be infinite, we propose several abstraction techniques for obtaining either an over-approximation or an under-approximation of the logical state space: (i) a folding abstraction that collapses patterns into more general ones, (ii) an easy-to-check method to define (bisimilar) equational abstractions, and (iii) an iterated bounded model checking method that can detect if a logical state space within a given bound is complete. We also show that folding abstractions can be faithful for safety LTL properties, so that they do not generate any spurious counterexamples. These abstraction methods can be used in combination and, as we illustrate with examples, can be effective in making the logical state space finite. We have implemented these techniques in the Maude system, providing the first narrowing-based LTL model checker we are aware of.

Microarchitectural refinements are often required to meet performance, area, or timing constraints when designing complex digital systems. While refinements are often straightforward to implement, it is difficult to formally specify the conditions of correctness for those which change cycle-level timing. As a result, in the later stages of design only those changes are considered that do not affect timing and whose verification can be automated using tools for checking FSM equivalence. This excludes an essential class of microarchitectural changes, such as the insertion of a register in a long combinational path to meet timing. A design methodology based on guarded atomic actions, or rules, offers an opportunity to raise the notion of correctness to a more abstract level. In rule-based systems, many useful refinements can be expressed simply by breaking a single rule into smaller rules which execute the original operation in multiple steps. Since the smaller rule executions can be interleaved with other rules, the verification task is to determine that no new behaviors have been introduced. We formalize this notion of correctness and present a tool based on SMT solvers that can automatically prove that a refinement is correct, or provide concrete information as to why it is not correct. With this tool, a larger class of refinements at all stages of the design process can be verified easily. We demonstrate the use of our tool in proving the correctness of the refinement of a processor pipeline from four stages to five.

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variant-based unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

We introduce the notion of well-founded recursive order-sorted equational logic (OS) theories modulo axioms. Such theories define functions by well-founded recursion and are inherently terminating. Moreover, for well-founded recursive theories important properties such as confluence and sufficient completeness are modular for so-called fair extensions. This enables us to incrementally check these properties for hierarchies of such theories that occur naturally in modular rule-based functional programs. Well-founded recursive OS theories modulo axioms contain only commutativity and associativity-commutativity axioms. In order to support arbitrary combinations of associativity, commutativity and identity axioms, we show how to eliminate identity and (under certain conditions) associativity without commutativity) axioms by theory transformations in the last part of the paper.

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.

This paper describes a formal executable semantics for the Verilog hardware description language. The goal of our formalization is to provide a concise and mathematically rigorous reference augmenting the prose of the official language standard, and ultimately to aid developers of Verilog-based tools; e.g., simulators, test generators, and verification tools. Our semantics applies equally well to both synthesizeable and behavioral designs and is given in a familiar, operational-style within a logic providing important additional benefits above and beyond static formalization. In particular, it is executable and searchable so that one can ask questions about how a, possibly nondeterministic, Verilog program can legally behave under the formalization. The formalization should not be seen as the final word on Verilog, but rather as a starting point and basis for community discussions on the Verilog semantics.

Abstract In model-driven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the meta-object facility (MOF) standard plays a crucial role as a generic framework within which a wide range of modeling languages can be defined. The MOF standard aims at offering a good basis for model-driven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. In this paper we define a reflective, algebraic, executable framework for precise metamodeling based on membership equational logic (mel) that supports the MOF standard. Our framework provides a formal semantics of the following notions:metamodel,model, andconformanceof a model to its metamodel. Furthermore, by using the Maude language, which directly supportsmelspecifications, this formal semantics isexecutable. This executable semantics has been integrated within the Eclipse modeling framework as a plugin tool called MOMENT2. In this way, formal analyses, such as semantic consistency checks, model checking of invariants and LTL model checking, become available within Eclipse to provide formal support for model-driven development processes.

The length of the microprocessor development cycle is largely determined by functional verification, where contemporary practice relies primarily on constraint-based random stimulus generation to drive a simulation-based methodology. However, formal methods are, in particular, gaining wider adoption and are seen as having potential to bridge large gaps left by current techniques. And many gaps still remain. In this paper we propose directed- logical testing: a new method of stimulus generation based on purely logical techniques (i.e. formal methods). As far as we know, our methodology represents the first end-to-end mathematical formalization of the stimulus generation problem. Therefore, a major contribution of this paper is the definition of a class of logical propositions that relate the actual microprocessor implementation, the assembly program stimulus, and a coverage goal. These propositions are given in rewriting logic, and use the idea of rewriting semantics to automatically formalize within a common logical framework the microprocessor implementation and assembly programs. To solve these propositions, we demonstrate how narrowing and user-defined narrowing strategies can be used as a scalable logical framework. In addition, we describe two classes of effective strategies that can be used for many microprocessors and common coverage goals. Finally, we describe a prototype tool implementation and present empirical data to demonstrate the feasibility of our methodology. Since narrowing and user-defined narrowing strategies within rewriting logic do not yet have tool support, our prototype tool uses standard rewriting and user-defined rewriting strategies to simulate narrowing.

Types (or sorts) are pervasive in computer science and in rewritingbased programming languages, which often support subtypes (subsorts) and subtype polymorphism. Programs in these languages can be modeled as order-sorted term rewriting systems (OS-TRSs). Often, termination of such programs heavily depends on sort information. But few techniques are currently available for proving termination of OS-TRSs; and they often fail for interesting OS-TRSs. In this paper we generalize the dependency pairs approach to prove termination of OS-TRSs. Preliminary experiments suggest that this technique can succeed where existing ones fail, yielding easier and simpler termination proofs

Orc is a language proposed by Jayadev Misra [19] for orchestration of distributed services. Orc is very simple and elegant, based on a few basic constructs, and allows succinct and understandable programming of sophisticated applications. However, because of its real-time nature and the different priorities given to internal and external events in an Orc program, giving a formal operational semantics that captures the real-time behavior of Orc programs is nontrivial and poses some interesting challenges. In this paper we propose such a real-time operational Orc semantics, that captures the informal operational semantics given in [19]. This operational semantics is given as a rewrite theory in which the elapse of time is explicitly modeled. The priorities between internal and external events are also modeled in two alternative ways: (i) by a rewrite strategy; and (ii) by adding extra conditions to the semantic rules. Since rewriting logic has efficient implementations such as Maude, we also get, directly out of the semantic definitions, both an Orc interpreter and an LTL model checker for Orc programs.

To achieve end-to-end security, traditional machine-to-machine security measures are insufficient if the integrity of the human-computer interface is compromised. GUI logic flaws are a category of software vulnerabilities that result from logic bugs in GUI design/implementation. Visual spoofing attacks that exploit these flaws can lure even security- conscious users to perform unintended actions. The focus of this paper is to formulate the problem of GUI logic flaws and to develop a methodology for uncovering them in software implementations. Specifically, based on an in-depth study of key subsets of Internet Explorer (IE) browser source code, we have developed a formal model for the browser GUI logic and have applied formal reasoning to uncover new spoofing scenarios, including nine for status bar spoofing and four for address bar spoofing. The IE development team has confirmed all these scenarios and has fixed most of them in their latest build. Through this work, we demonstrate that a crucial subset of visual spoofing vulnerabilities originate from GUI logic flaws, which have a well-defined mathematical meaning allowing a systematic analysis.

This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples.

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CafeOBJ, Maude, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as muterm, CiME, AProVE, TTT, Termptation, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned tools.

A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be good metalogical frameworks when their theories always have initial models and they support reflective and parameterized reasoning.We develop this thesis both abstractly and concretely. Abstractly, we formalize our proposal as a set of requirements and explain how any logic satisfying these requirements can be used for metalogical reasoning. Concretely, we present membership equational logic as a particular metalogic that satisfies these requirements. Using membership equational logic, and its realization in the Maude system, we show how reflection can be used for different, nontrivial kinds of formal metatheoretic reasoning. In particular, one can prove metatheorems that relate theories or establish properties of parameterized classes of theories.

An executable computational logic can provide the desired bridge between formal system properties and formal methods to verify them on the one hand, and executable models of system designs based on programming languages on the other. However, not all such logics are equally well suited for the task. This paper gives some requirements that seem important for a computational logic to be suitable in practice, and discusses the experience with rewriting logic, its Maude language implementation, and its formal tool environment, concluding that they seem to meet well those requirements.

Tile systems offer a general paradigm for modular descriptions of concurrent systems, based on a set of rewriting rules with side-effects. Monoidal double categories are a natural semantic framework for tile systems, because the mathematical structures describing system states and synchronizing actions (called configurations and observations, respectively, in our terminology) are monoidal categories having the same objects (the interfaces of the system). In particular, configurations and observations based on net-process-like and term structures are usually described in terms of symmetric monoidal and cartesian categories, where the auxiliary structures for the rearrangement of interfaces correspond to suitable natural transformations. In this paper we discuss the lifting of these auxiliary structures to double categories. We notice that the internal construction of double categories produces a pathological asymmetric notion of natural transformation, which is fully exploited in one dimension only (for example, for configurations or for observations, but not for both). Following Ehresmann (1963), we overcome this biased definition, introducing the notion of generalized natural transformation between four double functors (rather than two). As a consequence, the concepts of symmetric monoidal and cartesian (with consistently chosen products) double categories arise in a natural way from the corresponding ordinary versions, giving a very good relationship between the auxiliary structures of configurations and observations. Moreover, the Kelly–Mac Lane coherence axioms can be lifted to our setting without effort, thanks to the characterization of two suitable diagonal categories that are always present in a double category. Then, symmetric monoidal and cartesian double categories are shown to offer an adequate semantic setting for process and term tile systems.

Place/transition (PT) Petri nets are one of the most widely used models of concurrency. However, they still lack, in our view, a satisfactory semantics: on the one hand the ‘token game’ is too intensional, even in its more abstract interpretations in terms of nonsequential processes and monoidal categories; on the other hand, Winskel's basic unfolding construction, which provides a coreflection between nets and finitary prime algebraic domains, works only for safe nets. In this paper we extend Winskel's result to PT nets. We start with a rather general category PTNets of PT nets, we introduce a category DecOcc of decorated (nondeterministic) occurrence nets and we define adjunctions between PTNets and DecOcc and between DecOcc and Occ, the category of occurrence nets. The role of DecOcc is to provide natural unfoldings for PT nets, i.e., acyclic safe nets where a notion of family is used to relate multiple instances of the same place. The unfolding functor from PTNets to Occ reduces to Winskel's when restricted to safe nets. Moreover, the standard coreflection between Occ and Dom, the category of finitary prime algebraic domains, when composed with the unfolding functor above, determines a chain of adjunctions between PTNets and Dom.

The failure to make explicit two different notions of subtype, a subtype as inclusion notion originally proposed by Goguen and a subtype as implicit conversion notion originally proposed by Reynolds, leads to unsatisfactory situations in present approaches to subtyping. Here, it is argued that choosing either notion at the expense of the other would be mistaken and limiting, and a framework is proposed in which two subtype relations τ ≤ τ1 (inclusion) and τ ≤ : τ1 (implicit conversion) are distinguished and integrated. Part I generalizes the first-order equarional logic with subtypes as inclusions and overloaded function symbols from its usual set-theoretic semantics to a categorical semantics in the style of Lawvere. This provides a much more general notion of model and supports interpretations of a logic with subtypes in any category having a suitable canonical notion of subobject. Soundness and completeness of the logic in the categorical setting are proved, and the classifying category of a theory, which is the initial model in this context, is constructed in detail. The adjunction between theory presentations and model categories is also proved, shedding light on subtleties of operation overloading not present in the unsorted and many-sorted cases. All this sets the stage for the higher-order categorical semantics of subtypes developed in Part II.

The first-order theory of subtypes as inclusions developed in Part I is extended to a higher-order context. This involves providing a higher-order equational logic for (inclusive) subtypes, a categorical semantics for such a logic that is complete and has initial models, and a proof that this higher-order logic is a conservative extension of its first-order counterpart. This higher-order categorical semantics includes a new notion of homomorphism between models that is both very natural in terms of its preservation properties and substantially more general than other notions of higher-order homomorphism proposed previously. The categorical semantics of higher-order inclusive subtypes is then generalized to a notion of model with two subtype relations τ ≤ τ1 (inclusion) and τ ≤: τ1 (implicit conversion) thus reconciling and relating the two different intuitions that have so far prevailed in the first-order and higher-order cases. Axioms are then given that integrate the ≤ and ≤: relations in the unified categorical semantics. Besides enjoying the benefits provided by each of the notions without their respective limitations, this framework supports rules for structural subtyping that are more informative and can discriminate between inclusions and implicit conversions.

Although the mathematical foundations of relational databases are very well established, the state of affairs for object-oriented databases is much less satisfactory. We propose a semantic foundation for object-oriented databases based on a simple logic of change called rewriting logic, and a language called MaudeLog that is based on that logic. Some key advantages of our approach include its logical nature, its simplicity without any need for higher-order features, the fact that dynamic aspects are directly addressed, the rigorous integration of user-definable algebraic data types within the framework, the existence of initial models, and the integration of query, update, and programming aspects within a single declarative language.

Linear logic has recently been introduced by Girard as a logic of actions that seems well suited for concurrent computation. In this paper, we establish a systematic correspondence between Petri nets, linear logic theories, and linear categories. Such a correspondence sheds new light on the relationships between linear logic and concurrency, and on how both areas are related to category theory. Categories are here viewed as concurrent systems the objects of which are states, and the morphisms of which are transitions. This is an instance of the Lambek-Lawvere correspondence between logic and category theory that cannot be expressed within the more restricted framework of the Curry-Howard correspondence.

An algebraic axiomatization is proposed, where, given a net N, a term algebra P(N) with two operations of parallel and sequential composition is defined. The congruence classes generated by a few simple axioms are proved isomorphic to a slight refinement of classical processes. Actually, P(N) is a symmetric monoidal category, parallel composition is the monoidal operation on morphisms and sequential composition is morphism composition. Besides P(N), the authors introduce a category S(N) containing the classical occurrence and step sequences. The term algebras of P(N) and S(N) are in general incomparable, and thus they introduce two more categories, K(N) and T(N), providing a most concrete and a most abstract extremum, respectively. The morphisms of T(N) are proved isomorphic to the processes recently defined in terms of the swap transformation by E. Best and R. Devillers (Theor. Comput. Sci., vol.55, pp.87-136, 1987). Thus the diamond of the four categories gives a full account in algebraic terms of the relations between interleaving and partial ordering observations of place/transition net computations.>

A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and initiality theorems, and can be used to unify and relate many different notions of model that have been proposed in the literature, including those that extend the basic calculus with additional features such as fixpoints or a type of all types. Moreover, the polymorphic lambda calculus and Martin-Lof type theory are related by a map of logics. A categorical and initial model semantics is given for the basic calculus and for richer calculi that extend the basic one with fixpoints or with a type of all types.

This paper studies unification for order-sorted equational logic. This logic generalizes unsorted equational logic by allowing a partially ordered set of sorts, with the ordering interpreted as set-theoretic containment in the models; it also allows overloading of function symbols, such as + for integer and rational number addition, with the overloaded functions of greater rank interpreted in the models as extensions of those of smaller rank. Our presentation emphasizes semantic aspects, and gives a categorical treatment of unification that has substantial advantages in this context over the usual treatment of unifiers as endomorphisms of a single free algebra. Given system Γ of equations and a set E of axioms that is sort-preserving and does not impose restrictions on the sorts of its variables, the main results characterize when an order-sorted signature has a minimal (or finite, or most general when Γ is solvable) family of order-sorted E-unifiers for Γ. In addition, for unitary signatures, where each solvable system of equations has a most general unifier, we give a quasi-linear algorithm for syntactic unification (i.e., for E= ) a la Martelli-Montanari, that is more efficient than the unsorted one for failures.

The composition and extraction mechanisms of Petri nets are at present inadequate. This problem is solved by viewing place/transition Petri nets as ordinary, directed graphs equipped with two algebraic operations corresponding to parallel and sequential composition of transitions. A distributive law between the two operations captures a basic fact about concurrency. Novel morphisms are defined, mapping single, atomic transitions into whole computations, thus relating system descriptions at different levels of abstraction. Categories equipped with products and coproducts (corresponding to parallel and nondeterministic compositions) are introduced for Petri nets with and without initial markings. It is briefly indicated how the approach yields function spaces and novel interpretations of duality and invariants. The results provide a formal basis for expressing the semantics of concurrent languages in terms of Petri nets and an understanding of concurrency in terms of algebraic structures over graphs and categories that should apply to other models and contribute to the conceptual unification of concurrency.>

The equationally complete proof system for “if-then-else” of Bloom and Tindell (this Journal, 12(1983), pp. 677–707) is extended to a complete proof system for many-sorted algebras with extra operations, predicates and equations among those. We give similar completeness results for continuous algebras and program schemes (infinite trees) by the methods of algebraic semantics. These extensions provide a purely equational proof system to prove properties of functional programs over user-definable data types.

Article Principles of OBJ2 Share on Authors: Kokichi Futatsugi Electrotechnical Laboratory, 1-1-4 Umezono, Sakura, Niibari, Ibaraki 305, Japan Electrotechnical Laboratory, 1-1-4 Umezono, Sakura, Niibari, Ibaraki 305, JapanView Profile , Joseph A. Goguen SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford University SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford UniversityView Profile , Jean-Pierre Jouannaud CRIN, Campus Scientifique, BP 239, 54506 Vandoeuvre-les-Nancy, Cedex, France CRIN, Campus Scientifique, BP 239, 54506 Vandoeuvre-les-Nancy, Cedex, FranceView Profile , José Meseguer SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford Universit SRI International, Menlo Park CA and Center for the Study of Language and Information, Stanford UniversitView Profile Authors Info & Claims POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1985 Pages 52–66https://doi.org/10.1145/318593.318610Online:01 January 1985Publication History 308citation447DownloadsMetricsTotal Citations308Total Downloads447Last 12 Months14Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

This paper discusses two main ideas, unwinding and inference control. While both concern computer security, they are not closely related to each other. Unwinding is a verification technique for general security requirements based on noninterference assertions as in [Goguen & Meseguer 82a]. The inference control problem concerns preventing inference of unauthorized information by combining authorized information. The main result in this paper is an unwinding theorem that gives a very simple necessary and sufficient condition for a system to satisfy the MLS security policy system. A subsidiary topic is secure interfaces, which we show how to treat with noninterferce assertions.

This paper addresses the problem of finding safe paths through a network, some of whose nodes may be faulty. By a safe path we mean one between two nodes that does not contain any faulty node. The kinds of faults that concern us are not limited to those that may cause a failure of a node or link, but include those that may cause a node to distort messages in arbitrary ways. Furthermore, we want a distributed algorithm to allow the network itself to discover suitable paths without depending on a central controller for the analysis. More broadly, we assume that each node has only local knowledge of the network structure.

We assune that the reader is familiar with the ubiquity of information in the modern world and is sympathetic with the need for restricting rights to read, add, modify, or delete information in specific contexts. This need is particularly acute for systems having computers as significant components.