Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

TPP 2019 Mark in CafeOBJ- as an Example of Specification Verification -FUTATSUGI,Kokichi
二木 厚吉
JAIST(Japan Advanced Institute of Sciecne and Technology)
AIST (National Institute of Advanced Industrial Science and Technology)

1 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

What is Specification Verification?
CafeOBJ and Proof Scores
Theorem Proving vs Specification Verification
Specification Verification and Proof by Reduction

What is Specification Verification?
▶ Specification is a description of a model, and Specification

Verification is to show that the model has desirable
properties by deducing the properties from the specification.
▶ Specification Verification in this sense is theorem proving

where the specification is the set of axioms and the desirable
properties are theorems.
▶ “All models are wrong, some are useful.”▶ Specification Verification is a good (may be the strongest)

way for getting high-quality specifications (useful descriptionsof models).
▶ Specification Verification is still one of the most challenging

topics in software/system engineering.
2 / 27

Specification Verification
Answers to TPP 2019 Mark ProblemProof Scores for leads-to Properties
Concluding Remarks

What is Specification Verification?
CafeOBJ and Proof Scores
Theorem Proving vs Specification Verification
Specification Verification and Proof by Reduction

CafeOBJ (https://cafeobj.org/)▶ CafeOBJ is an executable algebraic specification language

system which can be used as a specification verification
system.
Proof Score Approach in CafeOBJ▶ Domain/requirement/design engineers are expected toconstruct proof scores (descriptions of proofs in CafeOBJ)
together with formal specifications.
▶ A proof score is an executable high level description- of an exhaustive symbolic test (i.e. a complete proof)- in equations (reduction rules) and reduction commands.

Proof by computation/reduction/rewriting

3 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

What is Specification Verification?
CafeOBJ and Proof Scores
Theorem Proving vs Specification Verification
Specification Verification and Proof by Reduction

Theorem Proving vs Specification Verification▶ The primary goal of Theorem Proving is to show that atheorem can be deduced from axioms with deduction rules.
Usually the axioms are already established ones.
▶ The primary goal of Specification Verification is to showthat a specification is complete enough to imply/infer
desirable properties. The specification (a set of axioms) aresupposed to be improved/refined through specification
verification.

4 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

What is Specification Verification?
CafeOBJ and Proof Scores
Theorem Proving vs Specification Verification
Specification Verification and Proof by Reduction

Specification Verification and Proof by Reduction▶ The final goal of Specification Verification is to get ahigh-quality specification (a set of axioms) which is reliable
enough to build important systems/services based on it.
▶ The main technical issue is systematic construction of areliable specification (a set of axioms).
▶ Proof by reduction/rewriting is a transparent

deduction/inference method, and contributes to ease theinherent diﬃculty of Specification Verification.

5 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,5
6 (1)Answer 1
1. Please formally define a notion of Turingmachines that manipulate cyclic tapes. A cyclic tape is a
fixed-length tape whose both ends are connected to eachother. You can base on any paper definition of Turingmachines.
-->--> Answer to 1.
--> The definition (specification) of Turing Machine with--> Cyclic Tape (TMCT) is given in the file ’tmct.cafe’.

6 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,5
6 (1)TMCT Transition Rules
ops ct nt : -> State . ops cs ns : -> Symbol .
vars SS1 SS2 : SeqSym . var SY : Symbol .
tr[l-1]: SS1 SY | ct cs | SS2 =>SS1 | nt SY | ns SS2 .
tr[l-2]: nilsym | ct cs | SS SY =>ns SS | nt SY | nilsym .
tr[nm]: nilsym | ct cs | nilsym =>nilsym | nt ns | nilsym .
tr[r-1]:
SS1 | ct cs | SY SS2 =>SS1 ns | nt SY | SS2 .
tr[r-2]: SY SS | ct cs | nilsym =>nilsym | nt SY | SS ns .

7 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,56 (1)Answer 2
2. Please definetheir one-step computation.
-->--> Answer to 2.
--> Transition rules defined in the modules--> TMCT-l-1 (tr[l-1]), TMCT-l-2 (tr[l-2]), TMCT-nm (tr[nm]),--> TMCT-r-1 (tr[r-1]), TMCT-r-2 (tr[r-2])--> define one-step computation of TMCT.
--> A concrete TMCT is specified as a finite set of--> transition rules each element of which is obtained from--> one of tr[l-1], tr[l-2], tr[nm], tr[r-1]), or tr[r-2]--> by instantiating ct, cs, nt, and ns.

8 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,5
6 (1)Answer 3
3. Please define the predicate that a machine halts on
a given input tape.
-->--> Answer to 3.
--> Let TMCT-1 be the given TMCT, and let cf be the--> configuration of TMCT-1 with the given input tape.
--> Then TMCT-1 starting from cf halts if and only if--> the following reduction halts.
-->
reduce in TMCT-1 : cf =(*,*)=>* CF:Cnfg .
--> Here the reduction successively prints out all the--> reachable configurations from cf.

9 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,5
6 (1)Answer 4
4. Please define a machine that, given aninput cyclic tape of unknown size and content, clears thetape and halts. You may assume a minimum length on inputtapes. This puzzle was given to me by Vincent van Oostrom.
-->--> Answer to 4.
--> TMCT CLR-l clears input symbols towards left and halts,--> and CLR-r clears input symbols towards right and halts.
--> CLR-l and CLR-r are specified in the file ’clr-lr.cafe’

10 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,5
6 (1)Answer 5
5. Please demonstrate how your machine above works on aconcrete tape example.
-->--> Answer to 5.
--> Examples of transitions (computations) of CLR-l, CLR-r,--> and (CLR-l + CLR-r) are given in--> the file clr-lr-tst.cafe.

11 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Answer 1
Answer 2,3
Answer 4,5
6 (1)Answer 6 (1)
6. (Optional) Please prove that your machine halts andresulting tape is cleared for any input cyclic tape.
-->--> Answer to 6.
--> Proof scores in the files tmct-szeqsz-ps.cafe,--> cnfg-is-istsis-ps.cafe, clr-l-tsis-lt-ts-ps.cafe,--> clr-r-ists-lt-ts-ps.cafe, and clr-lr-ts-imp-halt-ps--> prove that each of CLR-l and CLR-r clears input tape--> and halts with blank tape.

12 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Target systems▶ Target systems are supposed to be modeled as (possiblyinfinite state) transition systems.
▶ A transition system is specified with the following two entities.

(1) Abstract data types for defining state configurations ofthe transition system. The abstract data types are specified inequations which can also be conditional.
(2) Transitions that define behavior of the transition system.
The transitions are specified in transition rules which can also
be conditional.

13 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Target properties
The desirable properties of a transition system that are supposed
to be verified are invariant properties or leads-to properties.
▶ An invariant property is defined as a state predicate that

holds for all reachable states from initial states.
▶ A leads-to property is defined as a pair of state predicates(p,q), and defined to hold for a system if the system s entry to
the state where p holds implies that the system will surely get
into the state where q holds no matter what transition
sequence is taken. (p leads-to q) denotes that (p,q) is aleads-to property.

14 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Basic leads-to properties
A Basic leads-to property is defined as a pair of state predicates(p,q), and defined by the following two items. (p b-leads-to q)
denotes that (p,q) is a basic leads-to property.
▶ If s is a reachable state with (p(s) and (not q(s))), then (1)s has at least one next state, and (2) (p(s ′ ) or q(s ′ )) holds

for any next state s ′ of s.

▶ There exits no infinite transition sequence sq such that (1) itstarts with a reachable state, and (2) (p(s) and (not q(s)))
holds for any element state s of sq.

15 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Verification Conditions for Basic leads-to Properties
Let p,q be state predicates of a transition system T , let State be
set of states of T , let TRT ⊆ State×State be the set of one-steptransitions of T , and let Nat be the set of natural numbers.
If an invariant inv of T and an operator m of rank ’State ->Nat’ are defined such that the following two conditions hold, then(p b-leads-to q) holds.
(1) (∀(s,s ′ ) ∈ TRT((inv(s) and p(s) and (not q(s))) implies((p(s ′ ) or q(s ′ )) and (m(s) > m(s ′ )))))(2) (∀s ∈ State((inv(s) and p(s) and (not q(s))) implies(∃s ′ ∈ State((s,s ′ ) ∈ TRT ))))
(1) is called inductive leads-to condition，and condition (2)is called continuous leads-to condition.
16 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Verification Conditions for leads-to Properties
Let p,q,r be state predicates of a transition system T ,let (p -b>T q) denote that (p b-leads-to q) holds for T ,and let (p ->T q) denote that (p leads-to q) holds for T .
The following 4 items give verification consitions of (p ->T q)
based on (p -b>T q).
(1) (p -b>T q) implies (p ->T q)(2) ((p ->T q) and (q ->T r )) implies (p ->T r )(3) ((p ->T r ) and (q ->T r )) implies ((p or q) ->T r )(4) ((p ->T r ) or (q ->T r )) implies ((p and q) ->T r )17 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Answer 6 (2)--> The file tmct-szeqsz-ps.cafe proves that--> for any configuration cf of any TMCT,-->(size(cf) = size(cf’))--> holds for any configuration cf’ that is reachable--> from cf.
require tmct-szeqsz-ps

18 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Answer 6 (3)--> The file cnfg-is-istsis-ps.cafe proves that-->(is..(_:Cnfg) leads-to tsis(_:Cnfg))--> and-->(is..(_:Cnfg) leads-to ists(_:Cnfg))--> hold for any TMCT including CRL-l and ClR-r.
require cnfg-is-istsis-ps

19 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Answer 6 (4)--> The file clr-l-tsis-lt-ts-ps.cafe proves that-->(tsis(_:Cnfg) leads-to ts..(_:Cnfg))--> holds at the CRL-l.
require clr-l-tsis-lt-ts-ps-->--> The file clr-r-ists-lt-ts-ps.cafe proves that-->(ists(_:Cnfg) leads-to ts..(_:Cnfg))--> holds at the CRL-r.
require clr-r-ists-lt-ts-ps

20 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Answer 6 (5)--> The file clr-lr-ts-imp-halt-ps.cafe proves that--> (ts..(_:Cnfg) leads-to (ts..(_:Cnfg) and halt(_:Cnfg)))--> holds for CLR-l and CLR-r.
require clr-lr-ts-imp-halt-ps.cafe

21 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Target Systems and Properties
leads-to properties
Verification Conditions for leads-to Properties
Answer 6 (2)-(6)Answer 6 (6)--> Hence it is proved that--> (is..(_:Cnfg) leads-to (ts..(_:Cnfg) and halt(_:Cnfg)))--> holds for CLR-l and CLR-r.
--> It implies that if CLR-l or CLR-r starts with a--> configuration cf such that (is..(cf) = true),--> i.e. cf with a tape with only input symbols,--> then it surely halt with a configuration cf’--> such that (ts..(cf’) = true),--> i.e. cf’ with a tape with only tape symbols,--> no matter what transition sequence it takes.

22 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Some achievements of CafeOBJ proof score approach
Coordinating Deduction and Search
Well-Founded Induction

CafeOBJ Proof Score approach has been applied to the following
kinds of problems and found usable.
▶ Some classical mutual exclusion algorithms▶ Some real time algorithms
e.g. Fischer s mutual exclusion protocol▶ Railway signaling systems▶ Authentication protocole.g. NSLPK, Otway-Rees, STS protocols▶ Practical sized e-commerce protocol of SET▶ UML semantics (class diagram + OCL-assertions)▶ Formal Fault Tree Analysis▶ Secure workflow models, internal control▶ Automatic non-stop software update protocols/systems▶ International standard for automotive software▶ Protocols for Cloud computing
23 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Some achievements of CafeOBJ proof score approach
Coordinating Deduction and Search
Well-Founded Induction

Coordinating Deduction and Search▶ Built-in search predicates provide eﬀective ways to do proof(1) by search for cases of small size, and (2) by deduction forcases of large or infinite size .
▶ The transparent proof structure has a potential to make“lemma finding” easier by analyzing the problem domain but
not detailed logical inference rules.
▶ “PTG (Proof Tree Generation) + RC/RPC (Refinement ofCases through Refinement of Proof Constants)” provide aneﬀective way to do deduction (proof tree generation) withsystematic search induced by refinement of state
configurations (through refinement of proof constants).

24 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Some achievements of CafeOBJ proof score approach
Coordinating Deduction and Search
Well-Founded Induction

Well-Founded Induction
Let T be a set of elements with a well-founded binary relation<wf . That is, there is no infinite sequence of elements t1 , t2 , t3 , · · ·such that ti+1 <wf ti (i ∈ {1, 2, 3 · · · }).
The principle of well-founded induction is stated as follows.
[Principle of Well-Founded Induction (Noetherian Induction)]
Let p be a predicate on T then(∀t ∈ Srt((∀t ′ <wf t(p(t ′ ))) implies p(t)))
implies (∀t ∈ Srt(p(t))).
That is, if p(t) whenever p(t ′ ) for all t ′ ∈T such that t ′ <wf t, thenp(t) for all t∈T .

25 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Some achievements of CafeOBJ proof score approach
Coordinating Deduction and Search
Well-Founded Induction

Well-Founded Induction in CafeOBJ▶ The well-founded induction in CafeOBJ combines the termrefinement of and the induction on c1,c2,..,cn, and has apotential to support a variety of induction schemes.
▶ Theorem of Constants, Casesplit with Equations, Term

Refinement with Equations, Specification Calculus inCafeOBJ justify the well-founded induction naturally.

26 / 27

Specification Verification
Answers to TPP 2019 Mark Problem
Proof Scores for leads-to Properties
Concluding Remarks

Some achievements of CafeOBJ proof score approach
Coordinating Deduction and Search
Well-Founded Induction

Introduction to Specification Verification with CafeOBJ
27 / 27