Abstraction and automation for model management

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

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.