Critical flaws continue to exist at the level of domain, requirement, and/or design specification, and specification verification (i.e. to check whether a specification has desirable properties) is still one of the most important challenges in software/system engineering. CafeOBJ is an executable algebraic specification language system and domain/requirement/design engineers can write proof scores in CafeOBJ for improving quality of specifications by the specification verification. This paper describes advances of the proof scores for the specification verification in CafeOBJ from the author’s point of view.

An assessment method is proposed to classify the reliability of business processes related to transactions into those with a high and low risk of inconsistency according to the checking status of transaction documents (such as an order form, a delivery slip, an invoice, a receipt). We show a method for objectively examining the reliability of business processes without relying solely on expert knowledge and experience. In practice, however, some departments in a company can be expected to execute transaction documents checking reliably, while others may not be able to. To cope with this, the method is extended so that assessment can be performed by reflecting the certainty of transaction documents checking for each department. Transaction documents checking for departments outside the company and outsourced departments can be excluded (such as a low-level department), and the risk of inconsistency in transaction documents can then be determined, thus improving the practicality of the assessment method.

Abstract 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.

Even though software systems in some domains are expected to provide continuous services, most of them must undergo some form of changes. It leads to the emergence of dynamic software updating, a technique for updating a running software system without incurring any downtime. One of the challenges of designing a correct dynamic update is to identify a set of update points where the update can be safely applied to a running system. In this paper, we present a formal approach to modeling dynamic software updates and use the formal model to identify safe update points. In our approach, we formalize dynamic updates as state machines, and verify by model checking a set of desired properties which the running system is expected to satisfy after being updated. If counterexamples are found, we exclude those states that cause the counterexamples, and do model checking again. The process is iterated until all desired properties are successfully verified. We then finally obtain a set of safe update points. A case study is also presented to demonstrate the feasibility of the proposed approach.

The constructor-based logics constitute the logical foundation of the so-called OTS/CafeOBJ method, a modelling, specification and verification method of the observational transition systems. The important role played in algebraic specifications by the initial algebras semantics is well known. Free models along presentation morphisms provide semantics for the modules with initial denotation in structured specification languages. Following Goguen and Burstall, the notion of logical system over which we build specifications is formalized as an institution. The present work is an institution-independent study of the existence of free models along sufficient complete presentation morphisms in logics with constructors in the signatures.

Dynamic Software Updating (DSU) is a promising software maintenance technique, which aims at updating running software systems on the fly without incurring any downtime. The systems that require dynamic updating usually require high reliability assurance. Incorrect updating may cause them to behave erratically and/or even crash, and hence results in dreadful loss. However, there are few approaches to the study of the correctness of dynamic updating. In this paper, we systematically discuss the correctness of dynamic updating from a formal perspective, and present a first algebraic approach to formal analysis of it. The basic idea is to formalize dynamic updating systems as rewrite systems, with which we can analyze dynamic updates e.g. verifying their desired properties, or detecting incorrect update points, etc. The formal analysis helps us understand the behaviors of updated systems before we apply updates to the running systems, and hence improves the reliability of the systems after being updated.

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.

This paper discusses how to model digital licenses as observational transition systems (OTSs) with CafeOBJ, a formal algebraic specification language. To extend the concept of licensing to cover various application domains of digital rights management, we first analyze the concepts of permission and obligation with some real-world examples which are not covered by current XML-based Rights Expression Languages (RELs), and then discuss how to formally specify licenses in terms of deontic and temporal logic with OTS/CafeOBJ method. Several important deontic and temporal modeling issues of licenses are also addressed for discussion. The proposed formal license language can be used not only for the formal specifications of licenses which capture both static observations and dynamic state transitions of the licenses, but also for the formal verification of licenses thanks to the executability and theorem proving facility of CafeOBJ.

Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method — the OTS/CafeOBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method.

We describe a method of automating invariant verification of behavioral specifications, which are algebraic specifications of abstract machines. The proposed method is based on fixed-point computation, which is one of the standard techniques for automatic (invariant) verification. The proposed method has some notable features. Among them are as follow: (1) the method finds and uses as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed, and (2) the method finds a counterexample showing that an abstract machine does not satisfy an invariant property if any, which does not need to make the (reachable) state space of the abstract machine finite. Crème is a tool based on the proposed method. We also report on two case studies in which (1) Crème proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property and (2) Crème finds a counterexample showing that the NSPK authentication protocol does not satisfy the secrecy property.

Verifying specifications is still one of the most important undeveloped research topics in software engineering. It is important because quite a few critical bugs are caused at the level of domains, requirements, and/or designs. It is also important for the cases where no program codes are generated and specifications are analyzed and verified only for justifying models of problems in real world. This paper gives a survey of our research activities in verifying specifications with proof scores in CafeOBJ. After explaining fundamental issues and importance of verifying specifications, an overview of CafeOBJ language, the proof score approach in CafeOBJ including its applications to several areas are given. This paper is based on our already published books or papers (Diaconescu and Futatsugi, 1998; Futatsugi et al., 2005), and refers to many of our related publications. Interested readers are invited to look into them

Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find "bugs" in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.

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.

TLS has been formally analyzed with the OTS/CafeOBJ method. In the method, distributed systems are modeled as transition systems, which are written in terms of equations, and it is verified that the models have properties by means of equational reasoning. TLS is the latest version, or the successor of SSL, which is probably the most widely deployed security protocol. Among the results of the analysis are that pre-master secrets cannot be leaked, when a client has negotiated a cipher suite and security parameters with a server, the server has really agreed on them, and client cannot be identified if they do not send their certificates to servers

Chocolat/SMV is a translator that takes a CafeOBJ specification of a transition system called an OTS and generates an SMV specification of a finite version of the OTS. The primary purpose of the translation is to find errors lurked in CafeOBJ specifications of OTSs with SMV.

Service discovery is one key aspect in the enabling technologies for service-oriented system architecture. Current distributed technologies such as CORBA and Web services define a communication protocol for advertising and discovering services but less attention has been paid to service descriptions themselves. The paper proposes attribute-based templates for describing service descriptions. The templates are a compilation of the results from an empirical study on descriptions of software components advertised on the Internet and the attributes listed by related literature. Although the templates should not be considered complete, they act as a common guideline to assist service providers with the specification of their services, and can be adopted by implementations of description repositories. By having a common guideline, services are described in a more uniform way and client enterprises will also have a more consistent view of service descriptions and a more extensive set of information that is useful for service selection.

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 de-scribe real-time systems and verify their properties. Con-cretely, we evolve UNITY computational models by intro-ducing so-called clock variables so as to model real-time systems, describe a specification of a railroad crossing sys-tem in CafeOBJ and verify that the system has a safety prop-erty based on the specification with the help of the CafeOBJ system. 1.

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 discuss a support tool for highly reliable component-based software development. The tool assures the high reliability of the output by verifying refinement and by generating connectors. The advantages of the tool are automated refinement verification and automated connector generation. As a software architecture for component-based software, we select the tree architecture, in which components are represented by a projection-style behavioral specification. The input of the tool is: (a) a requirement specification of the target software, (b) a refined specification specifying how to combine the components, and (c) the components themselves. (a) and (b) are projection-style behavioral specifications, while (c) are JavaBeans. The output of the tool is JavaBeans that are obtained by combining (c) and the generated connectors.

Component-based software development, in which software is developed by combining components and connectors, has gained in popularity because it can increase software productivity. To increase software productivity, components must be re-used, but to do so, we must select a software architecture. We propose a new software architecture called a "tree architecture". It is represented by a special class of algebraic behavioral specification called "projection-style behavioral specification". Recently, even component-based enterprise systems have been developed, so the importance of technologies to develop highly reliable component-based software has increased. We propose two such technologies using projection-style behavioral specification. One is a technology that assures the high reliability of connectors. The other is a technology that assures the consistency of software family evolution. The advantages of these technologies are that they can be automated.

Behavioral specifications are for specifying behavior of software or its components. We introduce a class of "sufficient" specifications "simply observable behavioral specifications". In the process where we add conditional equations to a behavioral specification until we obtain a simply observable behavioral specification, we can find requirements for forgettable conditions. Verification methods of behavioral properties have difficulty when target systems are complex. Induction may be necessary. Finding lemmas may be necessary. However, by using a "sufficient" specification "a simply observable behavioral specification", i.e. by capturing requirements sufficiently, the difficulty eases.

CAFE is the name of a network based environment now under development for supporting systematic creation, checking, verification, and maintenance of formal specifications. CAFE has an algebraic specification language called CafeOBJ as its main specification language, and adopts an algebraic specification paradigm as its foundation. CafeOBJ is a successor of the OBJ language, and has important new features for concurrency and behavioral specifications. Concurrency and behavior are specified based on rewriting logic and behavioral (hidden sorted) algebra respectively. These new features make it possible to provide powerful language constructs for formal object oriented specifications. CAFE is designed to be a network based environment. For sharing specification documents systematically over networks, a new document formatting language called Forsdonnet (FORmal Specification Document ON NETwork) is designed by extending HTML. Forsdonnet includes constructs for formal and informal specifications, commands for executing (prototyping) and cheeking/verifying CafeOBJ specifications, etc. Forsdonnet is designed to be based on already established standard network infrastructure components like HTML and Netscape Navigator. The paper gives an overview and design considerations of the CAFE environment, featuring mainly CafeOBJ and Forsdonnet languages.

A scenario-based object-oriented modeling method for algebraic specifications is proposed.The method is based on the integration of a new algebraic specification language, CafeOBJ, and a multiparadigm design notation, GIL0-2 (Generic Interaction Language for Objects).CafeOBJ is a successor of the algebraic specification language OBJ and supports object-oriented formal specifications based on hidden order sorted rewriting logic.GIL0-2 provides collaborations as well as classes of objects to capture behavioral aspects of scenarios in object-oriented modeling.Given a problem description of the system to develop, the proposed method provides guidelines for decomposing the problem into executable CafeOBJ specification modules through scenario-based object-oriented design in GIL0-2; the decomposition reflects the structure of the problem domain.The proposal also indicates how formal executable specification in CafeOBJ can be systematically obtained from the design in GIL0-2.

The authors specify an example system, XVT, using two formal specification languages, LOTOS and OBJ, in order to compare both specifications from the viewpoint of a user of specification languages. They can distinguish two parts in both specifications: a static part and a dynamic part. The authors specified the dynamic part with a CCS approach using LOTOS and with a FSM approach using OBJ. This allows them to compare both languages on how they solve specific systems.>

Article Stepwise refinement process with modularity Share on Authors: Ataru T. Nakagawa Electrotechnical Laboratory, l-l-4 Umezono, Tsukuba Science City, Ibaraki 305, JAPAN Electrotechnical Laboratory, l-l-4 Umezono, Tsukuba Science City, Ibaraki 305, JAPANView Profile , Kokichi Futatsugi Electrotechnical Laboratory, l-l-4 Umezono, Tsukuba Science City, Ibaraki 305, JAPAN Electrotechnical Laboratory, l-l-4 Umezono, Tsukuba Science City, Ibaraki 305, JAPANView Profile Authors Info & Claims ICSE '89: Proceedings of the 11th international conference on Software engineeringMay 1989 Pages 166–177https://doi.org/10.1145/74587.74611Online:15 May 1989Publication History 5citation316DownloadsMetricsTotal Citations5Total Downloads316Last 12 Months4Last 6 weeks0 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

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