Supporting case analysis with algebraic specification languages

Case analysis is essential for verification of computer systems by writing proof scores in algebraic specification languages. When case analysis is performed, it is indispensable to cover all cases and find basic predicates that can be used for splitting cases. We propose two methods to support case analysis, which concern the two things. The first method uses matrices to cover all cases. The matrices consist of predicates that come from transition rules' conditions and properties to be verified. If it is not sufficient to split cases with such matrices, we must find basic predicates in the specifications of computer systems to split cases more precisely. Given a set of basic predicates, the second method mostly automates this process, which also can help find necessary lemmas. A case study in which our methods are effectively applied to a railroad signaling system is also reported.