BACK TO INDEX

Publications of year 2021
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.
    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},
    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. Saswata Paul, Gul A. Agha, Stacy Patterson, and Carlos A. Varela. Verification of Eventual Consensus in Synod using a Failure-Aware Actor Model. In Proceedings of the 13th NASA Formal Methods Symposium (NFM 2021), 2021. Note: To appear. Keyword(s): 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.

    @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 = {Proceedings of the 13th NASA Formal Methods Symposium (NFM 2021)},
    year = 2021,
    pdf = {http://wcl.cs.rpi.edu/papers/NFM2021_paul.pdf},
    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= {To appear} 
    }
    


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, 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, 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: Tue May 25 18:07:51 2021
Author: cruzce.


This document was translated from BibTEX by bibtex2html