-
Camilo Castellanos,
Carlos A. Varela,
and Dario Correal.
ACCORDANT: A domain specific-model and DevOps approach for big data analytics architectures.
Journal of Systems and Software,
172:110869,
2021.
ISSN: 0164-1212.
Keyword(s): Software architecture,
Big data analytics deployment,
DevOps,
Domain-specific model,
Quality scenarios,
Performance monitoring.
Abstract: |
Big data analytics (BDA) applications use machine learning algorithms to extract valuable insights from large, fast, and heterogeneous data sources. New software engineering challenges for BDA applications include ensuring performance levels of data-driven algorithms even in the presence of large data volume, velocity, and variety (3Vs). BDA software complexity frequently leads to delayed deployments, longer development cycles, and challenging performance assessment. This paper proposes a Domain-Specific Model (DSM), and DevOps practices to design, deploy, and monitor performance metrics in BDA applications. Our proposal includes a design process, and a framework to define architectural inputs, software components, and deployment strategies through integrated high-level abstractions to enable QS monitoring. We evaluate our approach with four use cases from different domains to demonstrate a high level of generalization. Our results show a shorter deployment and monitoring times, and a higher gain factor per iteration compared to similar approaches. |
@article{castellanos-accordant-2020,
title = "ACCORDANT: A domain specific-model and DevOps approach for big data analytics architectures",
journal = "Journal of Systems and Software",
volume = "172",
pages = "110869",
year = "2021",
issn = "0164-1212",
doi = "https://doi.org/10.1016/j.jss.2020.110869",
url = "http://www.sciencedirect.com/science/article/pii/S0164121220302594",
pdf = {http://wcl.cs.rpi.edu/papers/accordant_2020.pdf},
author = "Camilo Castellanos and Carlos A. Varela and Dario Correal",
keywords = "Software architecture, Big data analytics deployment, DevOps, Domain-specific model, Quality scenarios, Performance monitoring",
abstract = "Big data analytics (BDA) applications use machine learning algorithms to extract valuable insights from large, fast, and heterogeneous data sources. New software engineering challenges for BDA applications include ensuring performance levels of data-driven algorithms even in the presence of large data volume, velocity, and variety (3Vs). BDA software complexity frequently leads to delayed deployments, longer development cycles, and challenging performance assessment. This paper proposes a Domain-Specific Model (DSM), and DevOps practices to design, deploy, and monitor performance metrics in BDA applications. Our proposal includes a design process, and a framework to define architectural inputs, software components, and deployment strategies through integrated high-level abstractions to enable QS monitoring. We evaluate our approach with four use cases from different domains to demonstrate a high level of generalization. Our results show a shorter deployment and monitoring times, and a higher gain factor per iteration compared to similar approaches."
}
-
Michael Giancola,
Selmer Bringsjord,
Naveen Sundar Govindarajulu,
and Carlos Varela.
Making Maximally Ethical Decisions via Cognitive Likelihood & Formal Planning.
Towards Trustworthy Artificial Intelligent Systems, ed. M. Ferreira (Springer),
2021.
Abstract: |
This chapter attempts to give an answer to the following question: Given an obligation and a set of potentially-inconsistent, ethically-charged beliefs, how can an artificially-intelligent agent ensure that its actions maximize the likelihood that the obligation is satisfied? Our approach to answering this question is in the intersection of several areas of research, including automated planning, reasoning with uncertainty, and argumentation. We exemplify our reasoning framework in a case study based on the famous, heroic ditching of US Airways Flight 1549, an event colloquially known as the “Miracle on the Hudson.” |
@article{giancola-making-2021,
title={Making Maximally Ethical Decisions via Cognitive Likelihood \& Formal Planning},
author={Giancola, Michael and Bringsjord, Selmer and Govindarajulu, Naveen Sundar and Varela, Carlos},
journal={Towards Trustworthy Artificial Intelligent Systems, ed. M. Ferreira (Springer)},
year = {2021},
abstract ={This chapter attempts to give an answer to the following question: Given an obligation and a set of potentially-inconsistent, ethically-charged beliefs, how can an artificially-intelligent agent ensure that its actions maximize the likelihood that the obligation is satisfied? Our approach to answering this question is in the intersection of several areas of research, including automated planning, reasoning with uncertainty, and argumentation. We exemplify our reasoning framework in a case study based on the famous, heroic ditching of US Airways Flight 1549, an event colloquially known as the “Miracle on the Hudson.”},
pdf ={http://wcl.cs.rpi.edu/papers/giancolamaking2021.pdf}
}
-
Baoluo Meng,
Daniel Larraz,
Kit Siu,
Abha Moitra,
John Interrante,
William Smith,
Saswata Paul,
Daniel Prince,
Heber Herencia-Zapana,
M. Fareed Arif,
Moosa Yahyazadeh,
Vidhya Tekken Valapil,
Michael Durling,
Cesare Tinelli,
and Omar Chowdhury.
VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System.
Systems,
9(1),
2021.
Keyword(s): cyber security,
formal verification,
assurance case.
Abstract: |
The ever-increasing complexity of cyber-physical systems is driving the need for assurance of critical infrastructure and embedded systems. However, traditional methods to secure cyber-physical systems—e.g., using cyber best practices, adapting mechanisms from information technology systems, and penetration testing followed by patching—are becoming ineffective. This paper describes, in detail, Verification Evidence and Resilient Design In anticipation of Cybersecurity Threats (VERDICT), a language and framework to address cyber resiliency. When we use the term resiliency, we mean hardening a system such that it anticipates and withstands attacks. VERDICT analyzes a system in the face of cyber threats and recommends design improvements that can be applied early in the system engineering process. This is done in two steps: (1) Analyzing at the system architectural level, with respect to cyber and safety requirements and (2) by analyzing at the component behavioral level, with respect to a set of cyber-resiliency properties. The framework consists of three parts: (1) Model-Based Architectural Analysis and Synthesis (MBAAS); (2) Assurance Case Fragments Generation (ACFG); and (3) Cyber Resiliency Verifier (CRV). The VERDICT language is an Architecture Analysis and Design Language (AADL) annex for modeling the safety and security aspects of a system’s architecture. MBAAS performs probabilistic analyses, suggests defenses to mitigate attacks, and generates attack-defense trees and fault trees as evidence of resiliency and safety. It can also synthesize optimal defense solutions—with respect to implementation costs. In addition, ACFG assembles MBAAS evidence into goal structuring notation for certification purposes. CRV analyzes behavioral aspects of the system (i.e., the design model)—modeled using the Assume-Guarantee Reasoning Environment (AGREE) annex and checked against cyber resiliency properties using the Kind 2 model checker. When a property is proved or disproved, a minimal set of vital system components responsible for the proof/disproof are identified. CRV also provides rich and localized diagnostics so the user can quickly identify problems and fix the design model. This paper describes the VERDICT language and each part of the framework in detail and includes a case study to demonstrate the effectiveness of VERDICT—in this case, a delivery drone. |
@article{mang-mdpi-verdict-2021,
author = {Meng, Baoluo and Larraz, Daniel and Siu, Kit and Moitra, Abha and Interrante, John and Smith, William and Paul, Saswata and Prince, Daniel and Herencia-Zapana, Heber and Arif, M. Fareed and Yahyazadeh, Moosa and Tekken Valapil, Vidhya and Durling, Michael and Tinelli, Cesare and Chowdhury, Omar},
title = {VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System},
journal = {Systems},
volume = {9},
year = {2021},
number = {1},
url = {https://www.mdpi.com/2079-8954/9/1/18},
pdf = {http://wcl.cs.rpi.edu/papers/systems-09-00018.pdf},
keywords = {cyber security, formal verification, assurance case},
abstract = {The ever-increasing complexity of cyber-physical systems is driving the need for assurance of critical infrastructure and embedded systems. However, traditional methods to secure cyber-physical systems—e.g., using cyber best practices, adapting mechanisms from information technology systems, and penetration testing followed by patching—are becoming ineffective. This paper describes, in detail, Verification Evidence and Resilient Design In anticipation of Cybersecurity Threats (VERDICT), a language and framework to address cyber resiliency. When we use the term resiliency, we mean hardening a system such that it anticipates and withstands attacks. VERDICT analyzes a system in the face of cyber threats and recommends design improvements that can be applied early in the system engineering process. This is done in two steps: (1) Analyzing at the system architectural level, with respect to cyber and safety requirements and (2) by analyzing at the component behavioral level, with respect to a set of cyber-resiliency properties. The framework consists of three parts: (1) Model-Based Architectural Analysis and Synthesis (MBAAS); (2) Assurance Case Fragments Generation (ACFG); and (3) Cyber Resiliency Verifier (CRV). The VERDICT language is an Architecture Analysis and Design Language (AADL) annex for modeling the safety and security aspects of a system’s architecture. MBAAS performs probabilistic analyses, suggests defenses to mitigate attacks, and generates attack-defense trees and fault trees as evidence of resiliency and safety. It can also synthesize optimal defense solutions—with respect to implementation costs. In addition, ACFG assembles MBAAS evidence into goal structuring notation for certification purposes. CRV analyzes behavioral aspects of the system (i.e., the design model)—modeled using the Assume-Guarantee Reasoning Environment (AGREE) annex and checked against cyber resiliency properties using the Kind 2 model checker. When a property is proved or disproved, a minimal set of vital system components responsible for the proof/disproof are identified. CRV also provides rich and localized diagnostics so the user can quickly identify problems and fix the design model. This paper describes the VERDICT language and each part of the framework in detail and includes a case study to demonstrate the effectiveness of VERDICT—in this case, a delivery drone.},
doi = {10.3390/systems9010018}
}
-
Ankita Bhaumik,
Airin Dutta,
Fotis Kopsaftopoulos,
and Carlos A. Varela.
Proving the Correctness of Multicopter Rotor Fault Detection and Identification Software.
In The 40th AIAA/IEEE Digital Avionics Systems Conference (DASC 2021),
October 2021.
Keyword(s): fault detection,
formal verification,
multicopter,
declarative programming,
Dafny.
Abstract: |
Applications for data-driven systems are expected to be correct implementations of the system specifications, but developers usually test against a few indicative scenarios to verify them. In the absence of exhaustive testing, errors may occur in real time scenarios, especially when dealing with large data streams from moving objects like multicopters, vehicles, etc. Model checking techniques also lack scalability and completeness. We present a novel approach based on some existing tools which enables a developer to write high level code directly as system specifications and simultaneously be able to prove the correctness of the generated code. We present a fault detection and identification (FDI) software development approach using declarative programming language: PILOTS. The grammar of PILOTS has been updated to enable easier syntax for threshold validation techniques. The failure detection model is described as high level specifications that the generated code has to adhere to. The complete FDI problem is formally specified using Hoare logic and proven correct using an automated proof assistant: Dafny. A case study of rotor failures in a hexacopter has been used to illustrate the approach and visualize the results. |
@InProceedings{bhaumik-dasc-2021,
author = {Ankita Bhaumik and Airin Dutta and Fotis Kopsaftopoulos and Carlos A. Varela},
title = {Proving the Correctness of Multicopter Rotor Fault Detection and Identification Software},
booktitle="The 40th AIAA/IEEE Digital Avionics Systems Conference (DASC 2021)",
year="2021",
month="October",
pdf = {https://wcl.cs.rpi.edu/papers/bhaumik_et_al_DASC2021.pdf},
keywords = {fault detection, formal verification, multicopter, declarative programming, Dafny},
abstract = {Applications for data-driven systems are expected to be correct implementations of the system specifications, but developers usually test against a few indicative scenarios to verify them. In the absence of exhaustive testing, errors may occur in real time scenarios, especially when dealing with large data streams from moving objects like multicopters, vehicles, etc. Model checking techniques also lack scalability and completeness. We present a novel approach based on some existing tools which enables a developer to write high level code directly as system specifications and simultaneously be able to prove the correctness of the generated code. We present a fault detection and identification (FDI) software development approach using declarative programming language: PILOTS. The grammar of PILOTS has been updated to enable easier syntax for threshold validation techniques. The failure detection model is described as high level specifications that the generated code has to adhere to. The complete FDI problem is formally specified using Hoare logic and proven correct using an automated proof assistant: Dafny. A case study of rotor failures in a hexacopter has been used to illustrate the approach and visualize the results.}
}
-
Baoluo Meng,
Saswata Paul,
Abha Moitra,
Kit Siu,
and Michael Durling.
Automating the Assembly of Security Assurance Case Fragments.
In Ibrahim Habli,
Mark Sujan,
and Friedemann Bitsch, editors,
Computer Safety, Reliability, and Security,
Cham,
pages 101-114,
2021.
Springer International Publishing.
ISBN: 978-3-030-83903-1.
Keyword(s): cyber security,
formal verification,
assurance case.
Abstract: |
This paper presents an approach and tools for automatic generation of security assurance case fragments using patterns for arguing the security of cyber physical systems. The fragments are generated using augmented Goal Structuring Notation (GSN) and can succinctly convey a system's resilience to cyber-threats specified in MITRE's Common Attack Pattern Enumeration and Classification (CAPEC). The GSN schema has been augmented with additional metadata that can be used for visually tracing back to component-level CAPEC threats from higher-level cyber security claims, enabling designers to easily locate flaws in a model when one or more claims cannot be substantiated. An implementation of the approach as a part of the Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT) toolchain has also been demonstrated along with a case study of a package delivery drone. |
@InProceedings{meng-safecomp-2021,
author="Meng, Baoluo and Paul, Saswata and Moitra, Abha and Siu, Kit and Durling, Michael",
editor="Habli, Ibrahim and Sujan, Mark and Bitsch, Friedemann",
title="Automating the Assembly of Security Assurance Case Fragments",
booktitle="Computer Safety, Reliability, and Security",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="101--114",
pdf = {http://wcl.cs.rpi.edu/papers/meng_safecomp_2021.pdf},
url = "https://link.springer.com/chapter/10.1007%2F978-3-030-83903-1_7",
keywords = {cyber security, formal verification, assurance case},
abstract="This paper presents an approach and tools for automatic generation of security assurance case fragments using patterns for arguing the security of cyber physical systems. The fragments are generated using augmented Goal Structuring Notation (GSN) and can succinctly convey a system's resilience to cyber-threats specified in MITRE's Common Attack Pattern Enumeration and Classification (CAPEC). The GSN schema has been augmented with additional metadata that can be used for visually tracing back to component-level CAPEC threats from higher-level cyber security claims, enabling designers to easily locate flaws in a model when one or more claims cannot be substantiated. An implementation of the approach as a part of the Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT) toolchain has also been demonstrated along with a case study of a package delivery drone.",
isbn="978-3-030-83903-1"
}
-
Saswata Paul,
Gul A. Agha,
Stacy Patterson,
and Carlos A. Varela.
Verification of Eventual Consensus in Synod using a Failure-Aware Actor Model.
In NASA Formal Methods,
Cham,
pages 249-267,
2021.
Springer International Publishing.
ISBN: 978-3-030-76384-8.
Keyword(s): formal verification,
Athena,
distributed systems,
distributed computing,
air traffic management,
consensus,
actor model.
Abstract: |
Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol—which does not assume a unique leader—under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus. First, a subset of the agents must behave correctly and not permanently fail until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod. |
@InProceedings{paul-nfm-2021,
author = {Saswata Paul and Gul A. Agha and Stacy Patterson and Carlos A. Varela},
title = {Verification of Eventual Consensus in Synod using a Failure-Aware Actor Model},
booktitle="NASA Formal Methods",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="249--267",
pdf = {http://wcl.cs.rpi.edu/papers/NFM2021_paul.pdf},
isbn = "978-3-030-76384-8",
keywords = {formal verification, Athena, distributed systems, distributed computing, air traffic management, consensus, actor model},
abstract = {Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol—which does not assume a unique leader—under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus. First, a subset of the agents must behave correctly and not permanently fail until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.}
}
-
Saswata Paul,
Stacy Patterson,
and Carlos Varela.
Formal Guarantees of Timely Progress for Distributed Knowledge Propagation.
In Marie Farrell and Matt Luckcuck, editors,
Proceedings Third Workshop on Formal Methods for Autonomous Systems, Virtual, 21st-22nd of October 2021,
volume 348 of Electronic Proceedings in Theoretical Computer Science,
pages 73-91,
2021.
Open Publishing Association.
Keyword(s): formal verification,
Athena,
distributed systems,
distributed computing,
air traffic management,
formal verification,
Athena,
distributed systems,
distributed computing,
air traffic management.
Abstract: |
Autonomous air traffic management (ATM) operations for urban air mobility (UAM) will necessitate the use of distributed protocols for decentralized coordination between aircraft. As UAM operations are time-critical, it will be imperative to have formal guarantees of progress for the distributed protocols used in ATM. Under asynchronous settings, message transmission and processing delays are unbounded, making it impossible to provide deterministic bounds on the time required to make progress. We present an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using theories of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays being less than two given values. We also showcase the development of a library of formal theories, that is tailored towards reasoning about timely progress in distributed protocols deployed in airborne networks, in the Athena proof assistant. |
@InProceedings{paul-fmas-2021,
author = {Paul, Saswata and Patterson, Stacy and Varela, Carlos},
year = {2021},
title = {Formal Guarantees of Timely Progress for Distributed Knowledge Propagation},
editor = {Farrell, Marie and Luckcuck, Matt},
booktitle = {Proceedings Third Workshop on Formal Methods for Autonomous Systems, Virtual, 21st-22nd of October 2021},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {348},
publisher = {Open Publishing Association},
pages = {73-91},
keywords = {formal verification, Athena, distributed systems, distributed computing, air traffic management},
doi = {10.4204/EPTCS.348.5},
pdf = {http://wcl.cs.rpi.edu/papers/FMAS2021_paul.pdf},
keywords = {formal verification, Athena, distributed systems, distributed computing, air traffic management},
abstract = {Autonomous air traffic management (ATM) operations for urban air mobility (UAM) will necessitate the use of distributed protocols for decentralized coordination between aircraft. As UAM operations are time-critical, it will be imperative to have formal guarantees of progress for the distributed protocols used in ATM. Under asynchronous settings, message transmission and processing delays are unbounded, making it impossible to provide deterministic bounds on the time required to make progress. We present an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using theories of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays being less than two given values. We also showcase the development of a library of formal theories, that is tailored towards reasoning about timely progress in distributed protocols deployed in airborne networks, in the Athena proof assistant.}
}
-
Vidhya Tekken Valapil,
Heber Herencia-Zapana,
Michael Durling,
Kristen Armstrong,
Saswata Paul,
Szabolcs Borgyos,
Abha Moitra,
and William Premerlani.
Towards Formalization of a Data Model for Operational Risk Assessment.
In The 40th AIAA/IEEE Digital Avionics Systems Conference (DASC 2021),
San Antonio, TX,
October 2021.
Note: Best Paper Award.
Keyword(s): high assurance,
air traffic management,
formal methods.
Abstract: |
Operational Risk Assessment (ORA) is a process used to demonstrate and verify that the resultant risk of a planned operation meets certain required safety standards. Subject matter experts (SME) from different domains often use different approaches and terminologies to design ORAs. This leads to long review cycles and creates potential for inconsistent understanding of risks and/or application of mitigations by different practitioners across the safety-risk-chain. In this paper, to formalize ORA data representation we propose a set of common terminologies to be used while capturing ORA data. The proposed terminologies trace to existing standards and to terminologies used in risk data visualization methodologies. We also present a formal data model for ORA, that uses the proposed terminologies, in SADL (Semantic Application Design Language), thereby allowing SMEs to capture their knowledge as formal artifacts that are amenable to machine manipulation and automation. Furthermore, since ORA data is often captured in an excel format, we illustrate the use of an excel template that uses the proposed terminologies, by capturing assessment data corresponding to an example use case scenario in the template. Finally, to enable visualization of the ORA data, we discuss representing them as Bowtie diagrams. A Bowtie diagram is a pictorial representation that captures the relationship between a hazard, its causes and its consequences in a given specific environment or system state. To enable the benefits of Bowtie representation we map the proposed ORA terminologies to elements in a Bowtie model. We illustrate visualization of the ORA data as a Bowtie diagram by generating a Bowtie diagram capturing the ORA data corresponding to the example use case scenario considered in the paper. |
@InProceedings{valapil-dasc-2021,
author = {Vidhya Tekken Valapil and Heber Herencia-Zapana and Michael Durling and Kristen Armstrong and Saswata Paul and Szabolcs Borgyos and Abha Moitra and William Premerlani},
title = {Towards Formalization of a Data Model for Operational Risk Assessment},
booktitle = {The 40th AIAA/IEEE Digital Avionics Systems Conference (DASC 2021)},
year = {2021},
address = {San Antonio, TX},
month = {October},
pdf = {http://wcl.cs.rpi.edu/papers/DASC2021_valapil.pdf},
keywords = {high assurance, air traffic management, formal methods},
note = {Best Paper Award},
abstract = {Operational Risk Assessment (ORA) is a process used to demonstrate and verify that the resultant risk of a planned operation meets certain required safety standards. Subject matter experts (SME) from different domains often use different approaches and terminologies to design ORAs. This leads to long review cycles and creates potential for inconsistent understanding of risks and/or application of mitigations by different practitioners across the safety-risk-chain. In this paper, to formalize ORA data representation we propose a set of common terminologies to be used while capturing ORA data. The proposed terminologies trace to existing standards and to terminologies used in risk data visualization methodologies. We also present a formal data model for ORA, that uses the proposed terminologies, in SADL (Semantic Application Design Language), thereby allowing SMEs to capture their knowledge as formal artifacts that are amenable to machine manipulation and automation. Furthermore, since ORA data is often captured in an excel format, we illustrate the use of an excel template that uses the proposed terminologies, by capturing assessment data corresponding to an example use case scenario in the template. Finally, to enable visualization of the ORA data, we discuss representing them as Bowtie diagrams. A Bowtie diagram is a pictorial representation that captures the relationship between a hazard, its causes and its consequences in a given specific environment or system state. To enable the benefits of Bowtie representation we map the proposed ORA terminologies to elements in a Bowtie model. We illustrate visualization of the ORA data as a Bowtie diagram by generating a Bowtie diagram capturing the ORA data corresponding to the example use case scenario considered in the paper.}
}