CISE Postdoctoral Research Associates: A Model Construction Tool Suite for Finite-State Verification Java (CCR)

9901605 Hatcliff，John M.Dwyer，MatthewSchmidt，David A.堪萨斯州立大学CSE博士后研究助理实验计算机科学：用于Java有限状态验证的模型构建工具套件现代软件系统通常是并发的、分布式的和高度复杂的，但它们必须是极其可靠和正确的。虽然最初应用于硬件系统，但有限状态验证(FSV)技术(例如模型检查)正在成为现代软件高质量保证自动化竞赛的领跑者。要应用FSV技术，必须创建软件系统行为的有限状态转换系统模型。要验证的模型和属性被提供给FSV工具，并且通过机械地枚举转换系统中的所有可达状态并检查该属性在每个状态下是否成立来执行验证。目前，软件的有限状态模型必须手工创建。手工编码复杂的语言功能，如参数化的通用模块、过程、线程和动态创建的程序数据和控制线程，既繁琐又容易出错，不会扩展到大型生产系统。在国家科学基金会支持的其他工作中，正在开发使用抽象解释和部分评估技术自动构建软件有限状态模型的技术、方法和工具。该研究助理正在协调Java软件模型构建工具套件的开发。该伙伴在项目的理论和实施方面与私人投资和合作伙伴密切合作，并负责监督初级研究生的实施工作。这些任务为合伙人在执行和领导基础和实验研究方面的成长提供了一条途径。

9901605Hatcliff, John M.Dwyer, MatthewSchmidt, David A.Kansas State UniversityCISE Postdoctoral Research Associates in Experimental Computer Science: A Model Construction Tool Suite for Finite-State Verification of JavaModern software systems are often concurrent, distributed, and highly complex, yet they must beextremely reliable and correct. Although originally applied to hardware systems, finite-state verification (FSV) techniques (e.g. model checking) are emerging as the front-runner in the race to automate high-quality assurance of modern software. To apply FSV techniques, one must create a finite-state transition system model of the software system's behavior. The model and a property to be verified are given to a FSV tool, and verification is performed by mechanically enumerating all reachable states in the transition system and checking that the property holds at each state. Currently, finite-state models of software must be created by hand. Hand-coding complex language features such as parameterized generic modules, procedures, threads, and dynamically created program data and threads of control is tedious and error-prone, and will not scale to large production systems.In other National Science Foundation supported work, techniques, methodologies, and tools are being developed for automatically constructing finite-state models of software using abstract interpretation and partial evaluation technology. The research associate is coordinating the development of a model construction tool suite for Java software. The associate is working closely with the PI and Co-PIs on both the theoretical and implementation aspects of the project and is responsible for supervising the implementation work of junior graduate students. These tasks provide an avenue for the associate's growth in performing and leading foundational and experimental research.