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

[9016005] hatcliff, John M.Dwyer, MatthewSchmidt, David A.堪萨斯州立大学cise实验计算机科学博士后研究助理：用于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.