Abstraction and automation for model management

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

Improving the dependability of hardware and software systems is widely recognized as one of the most important challenges in information technology today. Interest in reliability and security issues has grown tremendously as a consequence of relatively frequent and expensive failures. These can be far in space (i.e., failure of the Mars probe) close to home (TTC failure, problems with CIBC's and Royal Bank's transaction processing systems) or affecting half the continent (the 2003 East Coast blackout). Formal verification has long been advocated as the best solution for improving the reliability of hardware and software systems, but the inherent difficulty in applying formal methods in practice has historically limited their success outside of academia. I believe that the key to solving this problem is abstraction and automation. The proposal builds on two major industrial developments: the success of automated model checking techniques, routinely applied in hardware companies, such as Intel and AMD. and the increased usage of model-driven development which promises automated generation of correct-by-construction code, in software industry. The goal of the proposal is two-fold: (1) to build fundamental techniques to enable the application of model-checking to software systems; specifically, code; and (2) to create support for all aspects of formal reasoning about higher-level artifacts: models. This entails giving models formal semantics, synthesizing preliminary odels from behavioural properties and usage scenarios, dealing with inconsistency which inevitably occurs when multiple people attempt to describe the same systems, and many others. Whether we lift models from code or create them from requirements, we expect results of this proposal to be vital to the task of constructing higher-quality software systems.