CAREER: Towards a Rigorous Methodology for Engineering Robust Software Systems
职业生涯:为工程鲁棒软件系统建立严格的方法论
基本信息
- 批准号:2144860
- 负责人:
- 金额:$ 50.61万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Continuing Grant
- 财政年份:2022
- 资助国家:美国
- 起止时间:2022-02-01 至 2028-01-31
- 项目状态:未结题
- 来源:
- 关键词:
项目摘要
Modern software systems are deployed in a highly dynamic, evolving environment that may occasionally deviate from its expected behavior. For example, a therapist interacting with a radiation therapy machine may inadvertently perform a sequence of critical actions in an incorrect order; a communication network may experience a disruption and fail to deliver messages in time; or a malicious actor on the web may evolve and obtain a wider range of exploits over time. Ideally, a system that is robust would ensure that its most critical requirements are satisfied even under possible deviations in the environment. This project aims to systematize the development of robust software by elevating robustness as a first-class quality attribute that can be explicitly analyzed for and designed into a system. To this end, the project will lay a rigorous foundation for software robustness and develop a set of fundamental analysis and design techniques to support methodologies for engineering robust systems. The results of this research will be incorporated into software engineering and formal method classes at Carnegie Mellon University.This project will investigate (1) a formal notion of robustness for software systems and (2) specification and verification techniques to support activities for developing robust systems. In particular, the project will develop techniques for formally reasoning about the robustness of a system as an explicit property, to answer questions such as: How robust is the system against possible deviations in the environment? What deviations could result in the system violating a critical requirement? Given a pair of alternative designs, which one of them is more robust under what deviations? In addition, given a model of a system that is incapable of tolerating certain deviations, the project will develop techniques for robustifying the system, by automatically transforming the existing design into one that is robust against those deviations. Finally, the project will demonstrate the applicability and utility of robustness across multiple domains, in particular through two innovative applications of the proposed techniques: (1) robustness testing of security protocols and (2) robustification of a safety-critical interface.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
现代软件系统部署在一个高度动态的、不断发展的环境中,这个环境可能偶尔会偏离其预期的行为。例如,与放射治疗机交互的治疗师可能会无意中以不正确的顺序执行一系列关键动作;通信网络可能会出现中断并无法及时传递消息;或者网络上的恶意行为者可能会随着时间的推移而演变并获得更广泛的利用。理想情况下,一个强大的系统将确保即使在环境可能出现偏差的情况下也能满足其最关键的要求。本项目旨在通过将健壮性提升为可以明确分析和设计成系统的一流质量属性,使健壮性软件的开发系统化。为此,该项目将为软件健壮性奠定坚实的基础,并开发一套基本的分析和设计技术,以支持工程健壮系统的方法。本研究的成果将被纳入卡内基梅隆大学的软件工程和形式方法课程中。本项目将研究(1)软件系统健壮性的形式化概念和(2)支持开发健壮系统活动的规范和验证技术。特别是,该项目将开发技术,正式推理系统的鲁棒性作为一个明确的属性,回答问题,如:如何强大的是系统对环境中可能的偏差?哪些偏差可能导致系统违反关键要求?给定一对可供选择的设计,在什么样的偏差下,哪一个设计更稳健?此外,鉴于一个系统的模型不能容忍某些偏差,该项目将开发使系统稳健的技术,方法是将现有设计自动转换为对这些偏差稳健的设计。最后,该项目将展示跨多个领域的鲁棒性的适用性和实用性,特别是通过所提出的技术的两个创新应用:(1)安全协议的鲁棒性测试,以及(2)安全协议的鲁棒性-该奖项反映了NSF的法定使命,并通过使用基金会的知识价值和更广泛的影响审查进行评估,被认为值得支持的搜索.
项目成果
期刊论文数量(5)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Robustification of Behavioral Designs against Environmental Deviations
针对环境偏差的行为设计的鲁棒性
- DOI:10.1109/icse48619.2023.00046
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Zhang, Changjian;Saluja, Tarang;Meira-Góes, Rômulo;Bolton, Matthew;Garlan, David;Kang, Eunsuk
- 通讯作者:Kang, Eunsuk
Task Model Design and Analysis with Alloy
合金任务模型设计与分析
- DOI:
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Alcino Cunha, Nuno Macedo
- 通讯作者:Alcino Cunha, Nuno Macedo
Safe Environmental Envelopes of Discrete Systems
离散系统的安全环境范围
- DOI:
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Romulo Meira-Goes, Ian Dardik
- 通讯作者:Romulo Meira-Goes, Ian Dardik
Runtime Resolution of Feature Interactions through Adaptive Requirement Weakening
- DOI:10.1109/seams59076.2023.00025
- 发表时间:2023-05
- 期刊:
- 影响因子:0
- 作者:Simon Chu;Emma Shedden;Changjian Zhang;Rômulo Meira-Góes;Gabriel A. Moreno;D. Garlan;Eunsuk Kang
- 通讯作者:Simon Chu;Emma Shedden;Changjian Zhang;Rômulo Meira-Góes;Gabriel A. Moreno;D. Garlan;Eunsuk Kang
Fortis: A Tool for Analysis and Repair of Robust Software Systems
Fortis:用于分析和修复稳健软件系统的工具
- DOI:
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者:Changjian Zhang, Ian Dardik
- 通讯作者:Changjian Zhang, Ian Dardik
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Eunsuk Kang其他文献
Synthesis-Based Resolution of Feature Interactions in Cyber-Physical Systems
信息物理系统中特征交互的基于综合的解析
- DOI:
10.1145/3324884.3416630 - 发表时间:
2020 - 期刊:
- 影响因子:0
- 作者:
B. Gafford;Tobias Dürschmid;Gabriel A. Moreno;Eunsuk Kang - 通讯作者:
Eunsuk Kang
Alloy*: a general-purpose higher-order relational constraint solver
Alloy*:通用高阶关系约束求解器
- DOI:
- 发表时间:
2015 - 期刊:
- 影响因子:0.8
- 作者:
Aleksandar Milicevic;Joseph P. Near;Eunsuk Kang;D. Jackson - 通讯作者:
D. Jackson
Open Design Case Study - A Crowdsourcing Effort to Curate Software Design Case Studies
开放设计案例研究 - 众包努力策划软件设计案例研究
- DOI:
10.1109/icse-seet58685.2023.00008 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Chun Yong Chong;Eunsuk Kang;Mary Shaw - 通讯作者:
Mary Shaw
Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
强化学习控制器对网络物理系统偏差的容忍度
- DOI:
- 发表时间:
2024 - 期刊:
- 影响因子:0
- 作者:
Changjian Zhang;Parv Kapoor;Eunsuk Kang;Rômulo Meira;David Garlan;Akila Ganlath;Shatadal Mishra;N. Ammar - 通讯作者:
N. Ammar
Model-Based Security Analysis of a Water Treatment System
基于模型的水处理系统安全分析
- DOI:
- 发表时间:
2016 - 期刊:
- 影响因子:0
- 作者:
Eunsuk Kang;Sridhar Adepu;D. Jackson;A. Mathur - 通讯作者:
A. Mathur
Eunsuk Kang的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Eunsuk Kang', 18)}}的其他基金
Collaborative Research: FMitF: Track I: Designing Safe and Robust Human-machine Interactions with Fuzzy Mental Models
合作研究:FMitF:第一轨:利用模糊心理模型设计安全、鲁棒的人机交互
- 批准号:
2319317 - 财政年份:2023
- 资助金额:
$ 50.61万 - 项目类别:
Standard Grant
NSF Student Travel and Registration Grant for IEEE/ACM International Conference on Software Engineering 2022 (ICSE)
2022 年 IEEE/ACM 国际软件工程会议 (ICSE) 的 NSF 学生旅费和注册补助金
- 批准号:
2210676 - 财政年份:2022
- 资助金额:
$ 50.61万 - 项目类别:
Standard Grant
Collaborative Research: EAGER: Towards a Design Methodology for Software-Driven Sustainability
合作研究:EAGER:迈向软件驱动的可持续性设计方法
- 批准号:
2233871 - 财政年份:2022
- 资助金额:
$ 50.61万 - 项目类别:
Standard Grant
FMitF: Collaborative Research: Track I: Preventing Human Errors in Cyber-human Systems with Formal Approaches to Human Reliability Rating and Model Repair
FMITF:协作研究:第一轨道:通过人类可靠性评级和模型修复的正式方法防止网络人类系统中的人为错误
- 批准号:
1918140 - 财政年份:2019
- 资助金额:
$ 50.61万 - 项目类别:
Standard Grant
相似海外基金
Optimizing stroke prevention for older adults with atrial fibrillation: Towards rigorous evaluation and judicious application of a new device
优化患有房颤的老年人的中风预防:严格评估和明智地应用新设备
- 批准号:
10533363 - 财政年份:2020
- 资助金额:
$ 50.61万 - 项目类别:
Optimizing stroke prevention for older adults with atrial fibrillation: Towards rigorous evaluation and judicious application of a new device
优化患有房颤的老年人的中风预防:严格评估和明智地应用新设备
- 批准号:
10339378 - 财政年份:2020
- 资助金额:
$ 50.61万 - 项目类别:
Workshop: Towards Rigorous Verification & Validation of Predictive Computational Models in Mechanics of Materials; New York, New York; July 27, 2018
研讨会:迈向严格验证
- 批准号:
1812449 - 财政年份:2018
- 资助金额:
$ 50.61万 - 项目类别:
Standard Grant
CAREER: Towards a rigorous foundation for scheduling in modern systems
职业生涯:为现代系统中的调度奠定严格的基础
- 批准号:
0846025 - 财政年份:2009
- 资助金额:
$ 50.61万 - 项目类别:
Standard Grant
Towards a rigorous process for designing validated telecommunications systems software
制定经过验证的电信系统软件设计严格流程
- 批准号:
8976-2001 - 财政年份:2005
- 资助金额:
$ 50.61万 - 项目类别:
Discovery Grants Program - Individual
Towards a rigorous process for designing validated telecommunications systems software
制定经过验证的电信系统软件设计严格流程
- 批准号:
8976-2001 - 财政年份:2004
- 资助金额:
$ 50.61万 - 项目类别:
Discovery Grants Program - Individual
Towards a rigorous process for designing validated telecommunications systems software
制定经过验证的电信系统软件设计严格流程
- 批准号:
8976-2001 - 财政年份:2003
- 资助金额:
$ 50.61万 - 项目类别:
Discovery Grants Program - Individual
Towards a rigorous process for designing validated telecommunications systems software
制定经过验证的电信系统软件设计严格流程
- 批准号:
8976-2001 - 财政年份:2003
- 资助金额:
$ 50.61万 - 项目类别:
Discovery Grants Program - Individual
Towards a rigorous process for designing validated telecommunications systems software
制定经过验证的电信系统软件设计严格流程
- 批准号:
8976-2001 - 财政年份:2002
- 资助金额:
$ 50.61万 - 项目类别:
Discovery Grants Program - Individual
Towards a rigorous process for designing validated telecommunications systems software
制定经过验证的电信系统软件设计严格流程
- 批准号:
8976-2001 - 财政年份:2001
- 资助金额:
$ 50.61万 - 项目类别:
Discovery Grants Program - Individual