Hidden Logic

From FSL
Jump to: navigation, search

Hidden Logic
Grigore Rosu
PhD Thesis, University of California at San Diego
Abstract. Cleverly designed software often fails to satisfy its requirements strictly, but instead satisfies them behaviorally, in the sense that they appear to be satisfied under every experiment that can be performed on the system. It is therefore becoming increasingly important to develop powerful techniques for behavioral specification and verification of systems, especially in the design stage, where most of the errors appear.

The general context of this thesis is formal methods for software and/or hardware development. We will present a promising new logic together with a language to support it, with applications to various branches of computer science, especially to the specification and automated verification of object-oriented and concurrent systems.

The thesis can be roughly divided into three major parts. The first is dedicated to presenting hidden logic in an easy going and intuitive way, with many examples, to developing sound inference rules, including a series of non-trivial coinduction rules, and to presenting a specification language in the OBJ family, called BOBJ, supporting hidden logic and reasoning. The second part is on automation of behavioral reasoning; more precisely, it introduces the techniques called behavioral rewriting, behavioral coinductive rewriting and circular coinductive rewriting, which are implemented in BOBJ. The third and the last part relates to more theoretical aspects of the logic, including relationships with other formalisms and theories, such as information hiding, coalgebra, institutions, Birkhoff-like axiomatizability, and incompleteness.

Personal tools