Search

In the present study, we provide conditions for the existence of pushouts of signature morphisms in constructor-based order-sorted algebra, and then we prove that reducibility and termination of term rewriting systems are closed under pushouts. Under the termination assumption, reducibility is equivalent to sufficient-completeness, which is crucial for proving several important properties in computing for constructor-based logics such as completeness, existence of initial models and interpolation. In logic frameworks that are not based on constructors, sufficient-completeness is essential to establish the soundness of the induction schemes which are based on some methodological constructor operators. We discuss the application of our results to the instantiation of parameterized specifications.

We present in this paper an interpreter implemented in Maude for non-behavioral CafeOBJ specifications. This alternative implementation poses a number of advantages: (1) it allows Maude tools to be used with CafeOBJ specifications, (2) it improves the performance of some CafeOBJ commands, such as search, (3) it enriches CafeOBJ syntax with Maude syntax, and (4) it makes CafeOBJ easily extensible, since new commands and tools can be included and tested and, once they are sufficiently mature, can be considered for inclusion in the Lisp implementation of CafeOBJ. The current tool presents a number of improvements over the tool presented in previous papers: it supports principal sorts, all kinds of CafeOBJ views, and all the search predicates recently implemented in the system. These improvements have allowed us to run the most recent CafeOBJ specifications, hence proving the robustness of the tool. Moreover, we present case studies illustrating the power of the tool, focusing on the falsification and verification of the NSPK and QLOCK protocols, respectively.

Proof scores are documents of comprehensible plans to prove theorems. The proof score approach to systems analysis is a method in which proof scores are used to verify that systems enjoy properties (or analyze systems). In this paper, we describe a way to analyze electronic commerce protocols with the proof score approach, which has been developed and refined through several case studies conducted.

We report on a case study in which the OTS/CafeOBJ method is used to formalize and verify trace anonymity property of distributed systems. In this case study, the property of trace anonymity is formalized with the trace notations of observational transition systems (OTSs), and CafeOBJ language/system is used as an interactive theorem prover to verify that systems satisfy such property. The work presented in the paper follows the approach proposed in [3], in which I/O automaton and Larch prover are employed for handling trace anonymity.

We present in this paper CafeInMaude, an interpreter for non-behavioral CafeOBJ specifications. The interpreter has been implemented in Maude. This alternative implementation combines CafeOBJ specification and theorem proving capabilities with efficient and extensible Maude commands and tools. Hence, it makes it possible to use both CafeOBJ proof scores and reduction commands and Maude model checking, narrowing, or theorem proving capabilities with the same tool.

SAL is a toolkit for analyzing transition systems, providing several different tools. Among the tools are a BDD-based symbolic model checker (SMC) and an SMT-based infinite bounded model checker (infBMC). The unique functionality provided by SAL is k-induction, which is supported by infBMC. Given appropriate lemmas, infBMC can prove automatically by k-induction that an infinite-state transition system satisfies invariant properties. Maude is a specification language and system based on membership equational logic and rewriting logic. Maude is equipped with an on-the-fly explicit state model checker. The unique functionality provided by the Maude model checker supports inductive data types. We make a comparison of SAL (especially SMC and infBMC) and the Maude model checker by conducting case studies in which the Suzuki-Kasami distributed mutual exclusion algorithm is analyzed. The purpose of the comparison is to clarify some of the two tools' functionalities, especially the unique ones, through the case studies.

We provide an innovative development of algebraic specifications and proof scores in CafeOBJ by extending a base specification to the meta-level that includes infinite transition sequences. The infinite transition sequences are modeled using behavioral specifications with hidden sort, and make it possible to prove safety and liveness properties in a uniform way.

OBJ algebraic specification languages, for example, OBJ3, CafeOBJ and Maude, are formal specification languages which support several sophisticated functions to describe and verify large and complex specifications. Recently, the proof score method, which is an interactive formal verification method for OBJ languages, based on constructor-based algebras has been developed and several practical case studies have been reported. Sufficient completeness is one of the most important properties of constructor-based specifications, which guarantees the existence of initial models. In this study, we give a sufficient condition for sufficient completeness of constructor-based specifications based on the theory of term rewriting.

Generic proof scores for the generate & check method in CafeOBJ are described. The generic proof scores codify the generate & check method as parameterized modules in the CafeOBJ language independently of specific systems to which the method applies. Basic proof scores for a specific system can be obtained by instantiating the formal parameter modules of the parameterized modules with the actual specification modules of the specific system. The effectiveness of the generic proof scores is demonstrated by applying them to a couple of non-trivial examples.

An interactive theorem proving method for the verification of infinite state transition systems is described.

OBJ algebraic specification languages support automated equational reasoning based on term rewriting for interactive verification. The equational reasoning is sound but not always complete in general. In our previous work, we have given a condition for sound and complete equational reasoning for OBJ specifications and have proposed the notion of local equality predicates (LEP), which is not only used for verification but also used for description of specifications. In this study, we propose a method to prove termination and confluence of specifications with LEPs. Termination and confluence are important properties of term rewriting and are parts of the LEP condition. By using the proposed method, we can use nested LEPs for large and complex modules.

OBJ languages support semi-automated verification for algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination, confluence and sufficient completeness are important fundamental properties for the equational reasoning. In this article, we give light-weight methods for checking those properties in a modular way. We formalize the notion of hierarchical extension for constructor-based conditional algebraic specifications, and give sufficient conditions for those fundamental properties, which can be used for proving them incrementally.

We have intensively used proof scores to theorem prove that equational theory specifications of observational transition systems (OTSs) have properties. The paper describes a way to theorem prove that rewrite theory specifications of OTSs have invariant properties by proof score writing. The method may achieve a more faithfully seamless integration of model checking and theorem proving because no translation is needed for system specifications. The Lowe’s modification (NSLPK) of NSPK authentication protocol is used to describe the method.

Rewriting logic can represent dynamic behaviours of concurrent and/or reactive systems declaratively. Declarative descriptions in rewriting logic are expected to be amenable to analysis of interesting properties. The group-wide architecture based on the actor model is a specific concurrent reflective computation model based on “group-wide reflection”. It has a potential of modelling cooperative behaviours of several software modules or agents. This paper provides some basic considerations on methods of modelling the group-wide architecture in rewriting logic and a brief proof that the metalevel group of terms correctly represents the operational semantics of the group in terms of transitions of configurations.

CafeOBJ is an executable industrial strength multi-logic algebraic specification language which is a modern successor of OBJ and incorporates several new algebraic specification paradigms. In this paper we survey its logical foundations and present some of its methodologies.

Proof scores are instructions to a proof engine such that when executed, if everything evaluates as expected, then a desired theorem is proved. Proof scores hide the detailed calculations done by machines, while revealing the proof plan created by humans. Although proof scores are executalbe by machines, they are also for human beings to read for proving (or verifying) desired properties on a system of interest. The technique of proof scores was brought up by the OBJ/CafeOBJ community, and substantial developments were done after a reliable implementation of CafeOBJ language system was available. This paper give an overview of evolution of proof scores which have been done under the efforts of verifying vearious kinds of formal specifications in CafeOBJ.

The OTS/CafeOBJ method can be used to model, specify and verify distributed systems. Specifications are written in equations, which are regarded as rewrite rules and used to verify specifications. The usefulness of the method is demonstrated by applying the method to nontrivial problems such as electronic commerce protocols and railroad signaling systems. In this paper we describe a toolkit called Buffet, which assists verification in the method. Given predicates used to split cases and lemmas, Buffet automatically generates proofs (called proof scores) and checks the proof scores using the CafeOBJ system. Buffet also has facilities to display proof scores generated and verification results on a web browser.

The induction-guided falsification searches a bounded reachable state space of a transition system for a counterexample that the system satisfies an invariant property. If no counterexamples are found, it tries to verify that the system satisfies the property by mathematical induction on the structure of the reachable state space of the system, from which some other invariant properties may be obtained as lemmas. The verification and falsification process is repeated for each of the properties until a counterexample is found or the verification is completed. The NSPK authentication protocol is used as an example to demonstrate the induction-guided falsification.

CafeOBJ is a wide spectrum specification language based on multiple logical foundations. CafeOBJ can be used to specify dynamic as well as static aspects of systems including object-oriented and reactive systems and verify their properties with the help of the CafeOBJ system. In this paper, we show that CafeOBJ can be also used to describe real-time systems and verify their properties. Concretely, we evolve UNITY computational models by introducing so-called clock variables so as to model real-time systems, describe a specification of a railroad crossing system in CafeOBJ and verify that the system has a safety property based on the specification with the help of the CafeOBJ system.

CafeOBJ is a wide spectrum formal specification language based on multiple logical foundations: mainly initial and hidden algebra. A wide range of systems can be specified in CafeOBJ thanks to its multiple logical foundations. However, distributed real-time systems happen to be excluded from targets of CafeOBJ. The authors propose a method of modeling and verifying such systems based on CafeOBJ, together with timed evolution of UNITY computational models.

We report on a case study in which the Maude model checker has been used to analyze the Suzuki-Kasami distributed mutual exclusion algorithm with respect to the mutual exclusion property and the lockout freedom property. Maude is a specification and programming language/system based on membership equational logic and rewriting logic, equipped with model checking facilities. Maude allows users to use abstract data types, including inductively defined ones, in specifications to be model checked, which is one of the advantages of the Maude model checker. Hence, queues, which are used in the case study, do not have to be encoded in more basic data types. In the case study, the Maude model checker has found a counterexample that the algorithm is lockout free, which has led to one possible modification that makes the algorithm lockout free.

We report on a machine supported method for verifying safety properties of dynamic systems based on the first-order description of underlying state transition systems. By capturing a set of states by a state predicate, we can verify safety properties of infinite-state systems using predicate calculus in the set-theoretic iterative calculation of least fixpoints.

Publisher Summary This chapter gives an overview of the main features and methodologies, and, logical and mathematical foundations of CafeOBJ. CafeOBJ is an executable industrial strength algebraic specification language, which is a modern successor of OBJ and incorporating several new algebraic specification paradigms. CafeOBJ also permits equational specification modulo several equational theories such as associativity, commutativity, identity, idempotence, and combinations between all these. Behavioral specification of CafeOBJ provides a novel generalization of ordinary algebraic specification, which directly supports the proof theory through special language constructs, such as, hidden sorts, behavioral operations, behavioral coherence declarations for operations, and behavioral axioms. Rewriting logic specification in CafeOBJ is based on a simplified version of Meseguer's rewriting logic specification framework for concurrent systems, which gives a non-trivial extension of traditional algebraic specification towards concurrency. The chapter is devoted to CafeOBJ handling of non-determinism and gives very compact specifications of a sorting algorithm to illustrate how CafeOBJ can be used both for executing algorithms and for reasoning about the algorithm itself. Finally, the chapter is dedicated to the current CafeOBJ methodology for composing objects concurrently by using projection operations, and deals with synchronization between the components via a counter-with-switch example.

In this paper, we show how to write a LOTOS simulator using OBJ. Both syntax rules and their inference rules (axioms) of LOTOS can be formally specified by operator definition part and equation definition part in OBJ, respectively.

In this paper, we present techniques for automated verification of behavioural specifications using hidden algebra. Two non-trivial examples, the Alternating Bit Protocol and a snooping cache coherence protocol, are presented with complete specification code and proof scores for CafeOBJ verification system. The refinement proof based on behavioural coinduction is given for the first example, and the coherence proof based on invariance is given for the second.

We propose a method of formally analysing security protocols based on rewriting. The method is roughly as follows. A security protocol is modeled as an observational transition system, which is described in CafeOBJ. Proof scores showing that the protocol has safety (security) properties are then written in CafeOBJ and the proof scores are executed (rewritten) by the CafeOBJ system.

Coinduction (co-induction) is considered to be a standard method for verifications of behavioural properties. However, users have to find a candidate for behavioural congruence relation (hidden congruence) for using coinducion. For expecting automatic support for coinduction, the candidate behavioural congruence relation is usually contextual equality. It is shown that a contextual equality which is also a behavioural congruence coincides with behavioural equivalence. This implies that users usually should find the behavioural equivalence for using coinduction. In this paper, we are going to propose a more systematic coinduction method. From the definition, behavioural equivalence is the conjunction over observational results through all observational contexts. Usually, there are redundant observational contexts. By analyzing the structure of the set of all observational contexts, we can eliminate these redundant observational contexts. We propose GAC algorithm which generates the contextual equality which coincides with the behavioural equivalence by eliminating the redundant observational contexts. The GAC algorithm uses rewrite techniques for eliminating the redundant observational contexts. We name the coinduction based on this GAC algorithm “test set coinduction” .

This paper surveys the logical and mathematical foundations of CafeOBJ, which is a successor of the famous algebraic specification language OBJ but adds to it several new primitive paradigms such as behavioural concurrent specification and rewriting logic.We first give a concise overview of CafeOBJ. Then we focus on the actual logical foundations of the language at two different levels: basic specification and structured specification, including also the definition of the CafeOBJ institution. We survey some novel or more classical theoretical concepts supporting the logical foundations of CafeOBJ, pointing out the main results but without giving proofs and without discussing all mathematical details. Novel theoretical concepts include the coherent hidden algebra formalism and its combination with rewriting logic, and Grothendieck (or fibred) institutions. However, for proofs and for some of the mathematical details not discussed here we give pointers to relevant publications.The logical foundations of CafeOBJ are structured by the concept of institution. Moreover, the design of CafeOBJ emerged from its logical foundations, and institution concepts played a crucial rôle in structuring the language design.

http://www.springerlink.com/content/u222753gl333221p/; Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process. By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.