Construction and verification of problem models in behavioral specifications

点击翻译按钮获取中文摘要

The following two important problems about construction and verification of problem models are investigated :(1) How to set an appropriate abstraction level in constructions of problem models and/or specifications.(2) How to combine interactive theorem proving technique and automatic searching based model checking technique in a collaborative way.Based on empirical studies on constructing and verifying problem models in several areas like railway signaling systems, component software systems, secure authentication systems, and etc., we got the following results.(1) Based on language constructs supported by CafeOBJ language, we have found that the distinction of abstract data types and abstract process types plays an important role in setting appropriate level in modeling/specification phase. Modeling/specification of process types are found to be complex and difficult than abstract data types, and we propose OTS (Observational Transition System) as a simple but powerful scheme for modeling/specifying process types. OTS is shown to be an effective and usable scheme for process types after applying it to several cases.(2) After studying several cases we have done, we found that (i) interactive theorem proving is more effective for proving some property hold, and (ii) automatic model checking is more effective for proving the some property does not hold (i.e. for finding counter examples). Based on this observation, we designed and developed an interactive tool which can support interactive proof (of proving some property hold) by finding counter examples with a model checking technique.