Proving Behavioral Refinements of COL-specifications

The COL institution (constructor-based observational logic) has been introduced as a formal framework to specify both generationand observation-oriented properties of software systems. In this paper we consider behavioral refinement relations between COL-specifications taking into account implementation constructions. We propose a general strategy for proving the correctness of such refinements by reduction to (standard) first-order theorem proving with induction. Technically our strategy relies on appropriate proof rules and on a lifting construction to encode the reachability and observability notions of the COL institution.

• Type: Conference
• Year: 2006
• Where: BIRTHDAY
• Authors: Michel Bidoit, Rolf Hennicker
• Keywords: Applied Computing, Behavioral Refinement Relations, BIRTHDAY 2006, COL Institution, Constructor-based Observational Logic