VeTSpec: Verified Trustworthy Software Specification

现代社会面临着一个根本性的问题：它严重依赖的复杂、不断发展的软件系统的可靠性，无法通过诸如非正式散文规范和临时测试等已建立的非数学技术来保证。现代公司发展迅速，几乎没有时间进行代码分析和测试；并发和分布式程序无法通过传统测试方法进行充分评估；移动应用程序的用户忽视了应用软件修复；恶意用户越来越多地利用编程错误，导致重大安全中断。值得信赖、可靠的软件正变得越来越难实现，而新的业务和网络安全挑战使其变得越来越重要。开发人员使用抽象来应对复杂性：将系统分解为通过软件接口连接的组件和层。这些接口使用规范来描述：例如，英语文档；具有不同严格程度的测试套件；嵌入在编程语言中的静态类型；以及以各种逻辑编写的形式规范。在计算机科学中，尽管对抽象的重要性达成了广泛的共识，但规范经常被视为软件开发的事后考虑和障碍，而且很少被证明是正当的。正式规范作为工业软件设计过程的一部分还处于初级阶段。我的总体研究愿景是将科学的、数学的方法引入到现代软件系统的规范和验证中。我当前工作的一个基本统一主题是我独特地强调了正式规范对于手头的任务是合适的、得到了适当的评估并对现实世界的应用程序有用的含义。规范应该得到验证，并有适当的证据证明它们描述了它们应该描述的内容。这种验证可以有多种形式，从正式验证到系统测试，再到精确论证正式规范准确地捕获了英语标准。规范应该是有用的，确定对现在和未来的客户都是直观和有帮助的组成构件。规范应该恰到好处，在实现和客户端程序之间提供清晰的逻辑边界。VeTSpec有四个相关的目标，探索程序规范、真实世界程序库规范和机械化语言规范的不同优势，在每种情况下确定规范对现实世界应用程序合适、适当评估和有用的含义。目标A：关于并发和分布的易处理推理是一个长期存在的困难问题。我将为并发程序和分布式系统的验证规范发展基础理论，重点讨论基于原始原子命令的程序的安全属性，基于更复杂的原子事务用于软件事务内存和分布式数据库的程序的安全属性，以及进度属性。目标B：JavaScript是使用最广泛的动态语言，94.8%的网站使用它。它的动态性和复杂的语义使得它很难成为验证规范的目标。我将开发基于逻辑的分析工具，用于说明、验证和测试JavaScript程序，将理论结果与适当的工程工具开发结合在一起。目标C：现实世界编程语言的机械化规范已经确立。这样的规范很难维护，它们的使用也没有得到充分的探索。我将提供一个可维护的Java脚本机械化规范，以及基于该规范的系统测试生成。目标D：我将探索与雄心勃勃的VeTSpec目标相关的基本概念问题，将科学的、数学的方法引入现代软件系统的规范。

Modern society faces a fundamental problem: the reliability of complex, evolving software systems on which it critically depends cannot be guaranteed by the established, non-mathematical techniques, such as informal prose specification and ad-hoc testing. Modern companies are moving fast, leaving little time for code analysis and testing; concurrent and distributed programs cannot be adequately assessed via traditional testing methods; users of mobile applications neglect to apply software fixes; and malicious users increasingly exploit programming errors, causing major security disruptions. Trustworthy, reliable software is becoming harder to achieve, whilst new business and cyber-security challenges make it of escalating importance.Developers cope with complexity using abstraction: the breaking up of systems into components and layers connected via software interfaces. These interfaces are described using specifications: for example, documentation in English; test suites with varying degrees of rigour; static typing embedded in programming languages; and formal specifications written in various logics. In computer science, despite widespread agreement on the importance of abstraction, specifications are often seen as an afterthought and a hindrance to software development, and are rarely justified.Formal specification as part of the industrial software design process is in its infancy. My over-arching research vision is to bring scientific, mathematical method to the specification and verification of modern software systems. A fundamental unifying theme of my current work is my unique emphasis on what it means for a formal specification to be appropriate for the task in hand, properly evaluated and useful for real-world applications. Specifications should be validated, with proper evidence that they describe what they should. This validation can come in many forms, from formal verification through systematic testing to precise argumentation that a formal specification accurately captures an English standard. Specifications should be useful, identifying compositional building blocks that are intuitive and helpful to clients both now and in future. Specifications should be just right, providing a clear logical boundary between implementations and client programs.VeTSpec has four related objectives, exploring different strengths of program specification, real-world program library specification and mechanised language specification, in each case determining what it means for the specification to be appropriate, properly evaluated and useful for real-world applications.Objective A: Tractable reasoning about concurrency and distribution is a long-standing, difficult problem. I will develop the fundamental theory for the verified specification of concurrent programs and distributed systems, focussing on safety properties for programs based on primitive atomic commands, safety properties for programs based on more complex atomic transactions used in software transactional memory and distributed databases, and progress properties.Objective B: JavaScript is the most widespread dynamic language, used by 94.8% of websites. Its dynamic nature and complex semantics make it a difficult target for verified specification. I will develop logic-based analysis tools for the specification, verification and testing of JavaScript programs, intertwining theoretical results with properly engineered tool development.Objective C: The mechanised specification of real-world programming languages is well-established. Such specifications are difficult to maintain and their use is not fully explored. I will provide a maintainable mechanised specification of Javascript, together with systematic test generation from this specification.Objective D: I will explore fundamental, conceptual questions associated with the ambitious VeTSpec goal to bring scientific, mathematical method to the specification of modern software systems.