BACK TO INDEX

Publications of year 2021
Thesis
  1. Camilo Castellanos. Executable Architectural Models for Big Data Analytics Development and Deployment. PhD thesis, Universidad de Los Andes, 2021. Keyword(s): big data.
    Abstract:
    With recent big data analytics (BDA) proliferation, enterprises collect and transform data to perform predictive analyses on a scale that a few years ago was not possible. BDA methodologies involve business, analytics, and technology domains. Each domain deals with different concern at different abstraction levels, but current BDA development does not consider the formal integration among these domains. Hence, the deployment procedure usually implies rewriting code to be deployed on specific IT infrastructures to obtain software aligned to functional and nonfunctional requirements. Moreover, surveys have reported a high cost and error-prone transition between analytics development (data lab) and productive environments. This thesis explores the challenges faced by stakeholders in BDA application development and presents a domainspecific model (DSM) approach to design, validate, and generate BDA applications from an architectural perspective, bridging the gap between analytics and IT architecture domains. First, we report our survey results on BDA application deployment applied to BDA practitioners to identify current practices and challenges. Second, the ACCORDANT reference architecture with tactics and patterns catalog to facilitate BDA adoption. Next, we present ACCORDANT modeling framework, a DSM to design and deploy BDA applications via the specification of architectural inputs, functional, and deployment views. Then, we state an approach to specify and evaluate constraints using object constraints and semantic reasoning in BDA architectures conforming to ACCORDANT. Finally, we report the results of this proposal’s application based on case studies and a survey that compares our approach and other according to 34 respondents.

    @PhdThesis{castellanos-thesis-2021,
    author = {Castellanos, Camilo},
    title = {{Executable Architectural Models for Big Data Analytics Development and Deployment}},
    school = {Universidad de Los Andes},
    year = 2021,
    pdf = {http://wcl.cs.rpi.edu/papers/castellanos_thesis_2021.pdf},
    keywords = {big data},
    abstract = {With recent big data analytics (BDA) proliferation, enterprises collect and transform data to perform predictive analyses on a scale that a few years ago was not possible. BDA methodologies involve business, analytics, and technology domains. Each domain deals with different concern at different abstraction levels, but current BDA development does not consider the formal integration among these domains. Hence, the deployment procedure usually implies rewriting code to be deployed on specific IT infrastructures to obtain software aligned to functional and nonfunctional requirements. Moreover, surveys have reported a high cost and error-prone transition between analytics development (data lab) and productive environments. This thesis explores the challenges faced by stakeholders in BDA application development and presents a domainspecific model (DSM) approach to design, validate, and generate BDA applications from an architectural perspective, bridging the gap between analytics and IT architecture domains. First, we report our survey results on BDA application deployment applied to BDA practitioners to identify current practices and challenges. Second, the ACCORDANT reference architecture with tactics and patterns catalog to facilitate BDA adoption. Next, we present ACCORDANT modeling framework, a DSM to design and deploy BDA applications via the specification of architectural inputs, functional, and deployment views. Then, we state an approach to specify and evaluate constraints using object constraints and semantic reasoning in BDA architectures conforming to ACCORDANT. Finally, we report the results of this proposal’s application based on case studies and a survey that compares our approach and other according to 34 respondents.} 
    }
    


Articles in journal, book chapters
  1. 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." 
    }
    


  2. 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} 
    }
    


Conference articles
  1. 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.} 
    }
    


  2. 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" 
    }
    


  3. 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.} 
    }
    


  4. Saswata Paul, Stacy Patterson, and Carlos A. Varela. Formal Guarantees of Timely Progress for Distributed Knowledge Propagation. In Formal Methods for Autonomous Systems, 2021. Keyword(s): 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 = {Saswata Paul and Stacy Patterson and Carlos A. Varela},
    title = {Formal Guarantees of Timely Progress for Distributed Knowledge Propagation},
    booktitle="Formal Methods for Autonomous Systems",
    year="2021",
    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.} 
    }
    


  5. 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 2019), 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 2019)},
    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.} 
    }
    


Internal reports
  1. Saswata Paul, Gul A. Agha, Stacy Patterson, and Carlos A. Varela. Verification of Eventual Consensus in Synod using a Failure-Aware Actor Model. Technical report, Rensselaer Polytechnic Institute, Department of Computer Science, 2021. Note: This report is an extended version of the NASA Formal Methods Symposium 2021 proceedings paper. Keyword(s): Synod, Paxos, actor model, formal verification, distributed computing, distributed systems, Athena, formal verification, Athena, distributed systems, 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.

    @TechReport{paul-eventualsynod-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},
    institution = {Rensselaer Polytechnic Institute, Department of Computer Science},
    year = 2021,
    pdf = {http://wcl.cs.rpi.edu/papers/nfm2021_techRep.pdf},
    keywords = {Synod, Paxos, actor model, formal verification, distributed computing, distributed systems, Athena},
    eprint = {2103.14576},
    archivePrefix = {arXiv},
    keywords = {formal verification, Athena, distributed systems, 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.},
    note= {This report is an extended version of the NASA Formal Methods Symposium 2021 proceedings paper.} 
    }
    



BACK TO INDEX




Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Les documents contenus dans ces rpertoires sont rendus disponibles par les auteurs qui y ont contribu en vue d'assurer la diffusion temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gards par les auteurs et par les dtenteurs du copyright, en dpit du fait qu'ils prsentent ici leurs travaux sous forme lectronique. Les personnes copiant ces informations doivent adhrer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas tre rendus disponibles ailleurs sans la permission explicite du dtenteur du copyright.




Last modified: Thu Oct 7 21:43:00 2021
Author: pauls4.


This document was translated from BibTEX by bibtex2html