VeTSpec: Verified Trustworthy Software Specification

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