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.