Abstraction and automation for model management

提高硬件和软件系统的可靠性被广泛认为是当今信息技术最重要的挑战之一。由于相对频繁且代价高昂的故障，人们对可靠性和安全性问题的兴趣大大增加。这些事故可能发生在遥远的太空（例如火星探测器的故障），也可能发生在离地球很近的地方（TTC故障，加拿大商业银行和皇家银行的交易处理系统出现问题），或者影响半个大陆（2003年东海岸停电）。形式化验证长期以来一直被认为是提高硬件和软件系统可靠性的最佳解决方案，但是在实践中应用形式化方法的固有困难历来限制了它们在学术界之外的成功。我相信解决这个问题的关键是抽象和自动化。该提议建立在两大工业发展的基础上：自动模型检查技术的成功，这种技术通常应用于英特尔和AMD等硬件公司。在软件行业中，模型驱动开发的使用增加了，它承诺自动生成结构正确的代码。该建议的目标有两个：(1)构建基本技术，使模型检查能够应用于软件系统；具体来说,代码;(2)创建对高级工件（模型）的形式推理的所有方面的支持。这需要为模型提供形式化语义，从行为属性和使用场景中合成初步模型，处理当多人试图描述相同系统和许多其他系统时不可避免地发生的不一致。无论我们是从代码中提取模型还是从需求中创建模型，我们都期望这个建议的结果对于构建更高质量的软件系统是至关重要的。

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.