In the OTS/CafeOBJ method, software specifications are described in CafeOBJ executable formal specification language, and verification is done by giving scripts to the CafeOBJ system. The script is called a proof score. In this study, we propose a test case generator from an OTS/CafeOBJ specification together with a proof score. Our test case generator gives test cases by analyzing the proof score. The test cases are used to test whether an implementation satisfies the specification and the property verified by the proof score. Since a proof score involves important information for verifying a property, the generated test cases are also expected to be suitable to test the property.

Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol*.

In this paper, we give a denotational semantics of imperative programming languages as a CafeOBJ behavioral specification. Since CafeOBJ is an executable algebraic specification language, not only execution of programs but also semi-automatic verification of programs properties can be done. We first describe an imperative programming language with integer and Boolean types, called IPL. Next we discuss about how to extend IPL, that is, IPL with user-defined types. We give a notion of equivalent programs, which is defined by using the notion of the behavioral equivalence of behavioral specifications. We show a sufficient condition for the equivalence relation of programs, which reduces the task to prove programs to be equivalent.

This paper presents a strategy together with tool support for the translation of state machines from equational theories into rewrite theories, aiming at automatically generating rewrite theory specifications. Duplicate effort can be saved on specifying state machines both in equational theories and rewrite theories, when we incorporate the theorem proving facilities of CafeOBJ with the model checking facilities of Maude. Experimental results show that efficiencies of the generated specifications by the proposed strategy are significantly improved, compared with those that are generated by three other existing translation strategies.

There are two ways to describe a state machine as an algebraic specification: a behavioral specification and a rewrite specification. In this study, we propose a translation system from behavioral specifications to rewrite specifications to obtain a verification system which has the strong points of verification techniques for both specifications. Since our translation system is complete with respect to invariant properties, it helps us to obtain a counter-example for an invariant property through automatic exhaustive searching for a rewrite specification.

We propose a user-defined on-demand matching strategy, called O-matching, in which users can control the order of matching arguments of each operation symbol. In ordinary matching schemes it is not important to set the order of matching, however, in on-demand matching schemes, it is very important since an input term may be changed while doing the on-demand matching process. O-matching is suitable to combine with the E-strategy, which is a user-defined reduction strategy in which users can control the order of reducing arguments. We show a sufficient condition under which the E-strategy with O-matching is correct for head normal forms, that is, any reduced term is a head normal form.