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

CISE 博士后研究员：用于有限状态验证 Java (CCR) 的模型构建工具套件

• 批准号: 9901605
• 负责人: John Hatcliff
• 金额: $ 6.6万
• 依托单位: Kansas State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-09-01 至 2001-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9901605&HistoricalAwards=false
• 关键词: CISE; Postdoctoral; Research; Associates; Model

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.

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