BACK TO INDEX

Publications of year 2020
Books and proceedings
  1. Laurent Lefevre, Carlos A. Varela, George Pallis, Adel N. Toosi, Omer Rana, and Rajkumar Buyya, editors. 20th IEEE/ACM International Symposium on Cluster, Cloud and Internet Computing, CCGrid 2020, Melbourne, Victoria, Australia, May 11-14, 2020, 2020. IEEE. Note: Due to COVID 19, the conference will now physically take place in 2021. Keyword(s): distributed computing, cloud computing.
    @proceedings{varela-ccgrid-2020,
    editor = {Laurent Lefevre and Carlos A. Varela and George Pallis and Adel N. Toosi and Omer Rana and Rajkumar Buyya},
    title = {20th IEEE/ACM International Symposium on Cluster, Cloud and Internet Computing, CCGrid 2020, Melbourne, Victoria, Australia, May 11-14, 2020},
    booktitle = {CCGRID},
    publisher = {IEEE},
    year = {2020},
    note = {Due to COVID 19, the conference will now physically take place in 2021},
    url = {http://cloudbus.org/ccgrid2020/CCGrid2020-Proceedings-FrontMatter.pdf},
    keywords = {distributed computing, cloud computing},
    
    }
    


Articles in journal, book chapters
  1. Saswata Paul, Fotis Kopsaftopoulos, Stacy Patterson, and Carlos A. Varela. Towards Formal Correctness Envelopes for Dynamic Data-Driven Aerospace Systems. In Frederica Darema and Erik Blasch, editors, Handbook of Dynamic Data-Driven Application Systems. Springer, 2020. Note: To appear. Keyword(s): dddas, data streaming, cyber physical systems, formal verification.
    Abstract:
    Intelligent aerospace systems of the future are expected to be ``smarter'' and more self-sufficient in terms of self-diagnosis, self-healing, overall situational awareness, and safe navigation. This will be facilitated by access to a vast amount of real-time data from on-board sensors, other aircraft, ground stations, and satellites. Dynamic data-driven application systems (DDDAS) can be used to incorporate real-time data for creating high-fidelity models to aid in flight-diagnosis and decision-making. DDDAS techniques accommodate the fusion of dynamic-data, algorithms, computation, and interpretation, making them apposite for use in safety-critical cyber-physical systems. In safety-critical systems, it is important to have irrefutable system guarantees. Formal methods allow the development of machine-checked correctness proofs for such guarantees, facilitating the verification of such systems on infinite states. This chapter presents formal correctness envelopes, analogous to performance envelopes of an aircraft, which represent the operating conditions under which the guarantees regarding a system's properties hold. These correctness envelopes are data-driven, allowing them to be computed, quantified, and monitored in real-time. Examples of safety envelopes and progress envelopes, which represent subsets of the DDDAS state space where safety and progress guarantees of a system are valid respectively, have been discussed. Correctness sentinels are executable programs that use the notion of correctness envelopes to monitor real-time data-streams and detect the status of a system's state with respect to relevant envelopes during runtime. At any given point of time, correctness sentinels can provide useful information about which system properties can be guaranteed and with how much confidence.

    @InCollection{paul-hbdddas-2020,
    author = {Saswata Paul and Fotis Kopsaftopoulos and Stacy Patterson and Carlos A. Varela},
    title = {Towards Formal Correctness Envelopes for Dynamic Data-Driven Aerospace Systems},
    booktitle = {Handbook of Dynamic Data-Driven Application Systems},
    year = 2020,
    editor = {Frederica Darema and Erik Blasch },
    publisher = {Springer},
    keywords = {dddas, data streaming, cyber physical systems, formal verification},
    note = {To appear},
    abstract = {Intelligent aerospace systems of the future are expected to be ``smarter'' and more self-sufficient in terms of self-diagnosis, self-healing, overall situational awareness, and safe navigation. This will be facilitated by access to a vast amount of real-time data from on-board sensors, other aircraft, ground stations, and satellites. Dynamic data-driven application systems (DDDAS) can be used to incorporate real-time data for creating high-fidelity models to aid in flight-diagnosis and decision-making. DDDAS techniques accommodate the fusion of dynamic-data, algorithms, computation, and interpretation, making them apposite for use in safety-critical cyber-physical systems. In safety-critical systems, it is important to have irrefutable system guarantees. Formal methods allow the development of machine-checked correctness proofs for such guarantees, facilitating the verification of such systems on infinite states. This chapter presents formal correctness envelopes, analogous to performance envelopes of an aircraft, which represent the operating conditions under which the guarantees regarding a system's properties hold. These correctness envelopes are data-driven, allowing them to be computed, quantified, and monitored in real-time. Examples of safety envelopes and progress envelopes, which represent subsets of the DDDAS state space where safety and progress guarantees of a system are valid respectively, have been discussed. Correctness sentinels are executable programs that use the notion of correctness envelopes to monitor real-time data-streams and detect the status of a system's state with respect to relevant envelopes during runtime. At any given point of time, correctness sentinels can provide useful information about which system properties can be guaranteed and with how much confidence.} 
    }
    


Conference articles
  1. Shabbir Ahmed, Ahmad Amer, Carlos Varela, and Fotis Kopsaftopoulos. Data-Driven State Awareness for Fly-by-Feel Aerial Vehicles via Adaptive Time Series and Gaussian Process Regression Models. In Dynamic Data-Driven Application Systems (InfoSymbiotics/DDDAS 2020), Cambridge, MA, October 2020.
    Abstract:
    This work presents the investigation and critical assessment, within the framework of Dynamic Data Driven Applications Systems (DDDAS), of two probabilistic state awareness approaches for fly-by-feel aerial vehicles based on (i) stochastic adaptive time-dependent time series models and (ii) Bayesian learning via homoscedastic and heteroscedastic Gaussian process regression models (GPRMs). Stochastic time-dependent autoregressive (TAR) time series models with adaptive parameters are estimated via a recursive maximum likelihood (RML) scheme and used to represent the dynamic response of a self-sensing composite wing under varying flight states. Bayesian learning based on homoscedastic and heteroscedastic versions of GPRM is assessed via the ability to represent the nonlinear mapping between the flight state and the vibration signal energy of the wing. The experimental assessment is based on a prototype self-sensing UAV wing that is subjected to a series of wind tunnel experiments under multiple flight states.

    @InProceedings{ahmed-dddas-2020,
    author = {Shabbir Ahmed and Ahmad Amer and Carlos Varela and Fotis Kopsaftopoulos},
    title = {{Data-Driven State Awareness for Fly-by-Feel Aerial Vehicles via Adaptive Time Series and Gaussian Process Regression Models}},
    booktitle = {Dynamic Data-Driven Application Systems (InfoSymbiotics/DDDAS 2020)},
    year = 2020,
    address = {Cambridge, MA},
    month = {October},
    pdf = {http://wcl.cs.rpi.edu/papers/DDDAS2020_Ahmed.pdf},
    abstract = {This work presents the investigation and critical assessment, within the framework of Dynamic Data Driven Applications Systems (DDDAS), of two probabilistic state awareness approaches for fly-by-feel aerial vehicles based on (i) stochastic adaptive time-dependent time series models and (ii) Bayesian learning via homoscedastic and heteroscedastic Gaussian process regression models (GPRMs). Stochastic time-dependent autoregressive (TAR) time series models with adaptive parameters are estimated via a recursive maximum likelihood (RML) scheme and used to represent the dynamic response of a self-sensing composite wing under varying flight states. Bayesian learning based on homoscedastic and heteroscedastic versions of GPRM is assessed via the ability to represent the nonlinear mapping between the flight state and the vibration signal energy of the wing. The experimental assessment is based on a prototype self-sensing UAV wing that is subjected to a series of wind tunnel experiments under multiple flight states.} 
    }
    


  2. Camilo Castellanos, Boris Pérez, Darìo Correal, and Carlos A Varela. A Model-Driven Architectural Design Method for Big Data Analytics Applications. In 2020 IEEE International Conference on Software Architecture Companion (ICSA-C), pages 89-94, November 2020. IEEE. Keyword(s): distributed computing, distributed systems.
    Abstract:
    Big data analytics (BDA) applications use machine learning to extract valuable insights from large, fast, and heterogeneous data sources. The architectural design and evaluation of BDA applications entail new challenges to integrate emerging machine learning algorithms with cutting-edge practices whilst ensuring performance levels even in the presence of large data volume, velocity, and variety (3Vs). This paper presents a design process approach based on the Attribute-Driven Design (ADD) method and Architecture tradeoff analysis method (ATAM) to specify, deploy, and monitor performance metrics in BDA applications supported by domain-specific modeling and DevOps. Our design process starts with the definition of architectural drivers, followed by functional and deployment specification through integrated high-level modeling which enables quality scenarios monitoring. We used two use cases from avionics to evaluate this proposal, and the preliminary results suggest advantages by integrating multiple views, automating deployment and monitoring compared to similar approaches.

    @InProceedings{castellanos-icsa-2020,
    title = {A Model-Driven Architectural Design Method for Big Data Analytics Applications},
    author = {Castellanos, Camilo and P{\'e}rez, Boris and Correal, Dar{\'\i}o and Varela, Carlos A},
    booktitle = {2020 IEEE International Conference on Software Architecture Companion (ICSA-C)},
    pages = {89--94},
    year = {2020},
    month = {November},
    organization = {IEEE},
    keywords = {distributed computing, distributed systems},
    pdf = {http://wcl.cs.rpi.edu/papers/ICSA_2020.pdf},
    abstract = "Big data analytics (BDA) applications use machine learning to extract valuable insights from large, fast, and heterogeneous data sources. The architectural design and evaluation of BDA applications entail new challenges to integrate emerging machine learning algorithms with cutting-edge practices whilst ensuring performance levels even in the presence of large data volume, velocity, and variety (3Vs). This paper presents a design process approach based on the Attribute-Driven Design (ADD) method and Architecture tradeoff analysis method (ATAM) to specify, deploy, and monitor performance metrics in BDA applications supported by domain-specific modeling and DevOps. Our design process starts with the definition of architectural drivers, followed by functional and deployment specification through integrated high-level modeling which enables quality scenarios monitoring. We used two use cases from avionics to evaluate this proposal, and the preliminary results suggest advantages by integrating multiple views, automating deployment and monitoring compared to similar approaches." 
    }
    


  3. Elkin Cruz-Camacho, Saswata Paul, Fotis Kopsaftopoulos, and Carlos A. Varela. Towards Provably Correct Probabilistic Flight Systems. In Dynamic Data-Driven Application Systems (InfoSymbiotics/DDDAS 2020), Cambridge, MA, October 2020. Keyword(s): cyber physical systems, agda, formal verification, dddas.
    Abstract:
    Safety envelopes are meant to determine under which conditions and state space regions a probabilistic property of a data-driven system can be asserted with high confidence. Dynamic data-driven applications systems (DDDAS) can make use of safety envelopes to be cognizant of the formal warranties derived from their models and assumptions. An example of safety envelopes is presented as the intersection of two simpler concepts: z-predictability and Ï„-confidence; which correspond to state estimation and classification, respectively. To illustrate safety envelopes, stall detection from signal energy is shown with data gathered by piezo-electric sensors in a composite wing inside a wind tunnel under varying angles of attack and airspeed configuration. A formalization of these safety envelopes is presented in the proof assistant Agda, from which formally proven sentinel code can be generated.

    @InProceedings{cruz-dddas-2020,
    author = {Elkin Cruz-Camacho and Saswata Paul and Fotis Kopsaftopoulos and Carlos A. Varela},
    title = {Towards Provably Correct Probabilistic Flight Systems},
    booktitle = {Dynamic Data-Driven Application Systems (InfoSymbiotics/DDDAS 2020)},
    year = 2020,
    address = {Cambridge, MA},
    month = {October},
    keywords = {cyber physical systems, agda, formal verification, dddas},
    pdf = {http://wcl.cs.rpi.edu/papers/DDDAS2020_Cruz.pdf},
    abstract = {Safety envelopes are meant to determine under which conditions and state space regions a probabilistic property of a data-driven system can be asserted with high confidence. Dynamic data-driven applications systems (DDDAS) can make use of safety envelopes to be cognizant of the formal warranties derived from their models and assumptions. An example of safety envelopes is presented as the intersection of two simpler concepts: z-predictability and Ï„-confidence; which correspond to state estimation and classification, respectively. To illustrate safety envelopes, stall detection from signal energy is shown with data gathered by piezo-electric sensors in a composite wing inside a wind tunnel under varying angles of attack and airspeed configuration. A formalization of these safety envelopes is presented in the proof assistant Agda, from which formally proven sentinel code can be generated.} 
    }
    


  4. Anirban Das, Andrew Leaf, Carlos A. Varela, and Stacy Patterson. Skedulix: Hybrid Cloud Scheduling for Cost-Efficient Execution of Serverless Applications. In IEEE International Conference on Cloud Computing, Beijing, China, October 2020. Keyword(s): distributed computing, serverless computing, middleware.
    Abstract:
    We present a framework for scheduling multifunction serverless applications over a hybrid public-private cloud. A set of serverless jobs is input as a batch, and the objective is to schedule function executions over the hybrid platform to minimize the cost of public cloud use, while completing all jobs by a specified deadline. As this scheduling problem is NP-Hard, we propose a greedy algorithm that dynamically determines both the order and placement of each function execution using predictive models of function execution time and network latencies. We present a prototype implementation of our framework that uses AWS Lambda and OpenFaaS, for the public and private cloud, respectively. We evaluate our prototype in live experiments using a mixture of compute and I/O heavy serverless applications. Our results show that our framework can achieve a speedup in batch processing of up to 1.92 times that of an approach that uses only the private cloud, at 40.5% the cost of an approach that uses only the public cloud

    @InProceedings{das-ieee-cloud-2020,
    author = {Anirban Das and Andrew Leaf and Carlos A. Varela and Stacy Patterson},
    title = {Skedulix: Hybrid Cloud Scheduling for Cost-Efficient Execution of Serverless Applications},
    booktitle = {IEEE International Conference on Cloud Computing},
    year = 2020,
    address = {Beijing, China},
    month = {October},
    keywords = {distributed computing, serverless computing, middleware},
    url = {https://arxiv.org/abs/2006.03720},
    pdf = {http://wcl.cs.rpi.edu/papers/IEEE-cloud-2020_Das.pdf},
    abstract = {We present a framework for scheduling multifunction serverless applications over a hybrid public-private cloud. A set of serverless jobs is input as a batch, and the objective is to schedule function executions over the hybrid platform to minimize the cost of public cloud use, while completing all jobs by a specified deadline. As this scheduling problem is NP-Hard, we propose a greedy algorithm that dynamically determines both the order and placement of each function execution using predictive models of function execution time and network latencies. We present a prototype implementation of our framework that uses AWS Lambda and OpenFaaS, for the public and private cloud, respectively. We evaluate our prototype in live experiments using a mixture of compute and I/O heavy serverless applications. Our results show that our framework can achieve a speedup in batch processing of up to 1.92 times that of an approach that uses only the private cloud, at 40.5% the cost of an approach that uses only the public cloud} 
    }
    


  5. Michael Giancola, Selmer Bringsjord, Naveen Sundar Govindarajulu, and Carlos Varela. Ethical Reasoning for Autonomous Agents Under Uncertainty. In International Conference on Robot Ethics and Standards (ICRES) 2020, Taipei, Taiwan, September 2020.
    Abstract:
    Autonomous (and partially autonomous) agents are beginning to play significant roles in safetycritical and privacy-critical domains, such as driving and healthcare. When humans operate in these spaces, not only are there regulations and laws dictating proper behavior, but crucially, neurobiologically normal humans can be expected to comprehend how to reason with certain principles to ensure that their actions are legally/ethically/prudentially correct (whether or not these humans choose to abide by the principles in question). It seems reasonable that we should hold autonomous agents to, minimally, the same standard we hold humans to. In this paper, we present a framework for autonomous aircraft piloting agents to reason about ethical problems in the context of emergency landings. In particular, we are concerned with ethical problems in which every option is equally unethical with regard to the ethical principles the options violate; and the only distinguishing factor is the likelihood that a plan will violate an ethical principle. We conclude by discussing why, in general, we find an inference-theoretic approach to ethical reasoning to be superior to the model-theoretic approach of prior work.

    @InProceedings{giancola-ethical-2020,
    author = {Michael Giancola and Selmer Bringsjord and Naveen Sundar Govindarajulu and Carlos Varela},
    title = {Ethical Reasoning for Autonomous Agents Under Uncertainty},
    booktitle = {International Conference on Robot Ethics and Standards (ICRES) 2020},
    year = 2020,
    address = {Taipei, Taiwan},
    month = {September},
    pdf = {http://wcl.cs.rpi.edu/papers/ICRES2020-giancola.pdf},
    abstract = {Autonomous (and partially autonomous) agents are beginning to play significant roles in safetycritical and privacy-critical domains, such as driving and healthcare. When humans operate in these spaces, not only are there regulations and laws dictating proper behavior, but crucially, neurobiologically normal humans can be expected to comprehend how to reason with certain principles to ensure that their actions are legally/ethically/prudentially correct (whether or not these humans choose to abide by the principles in question). It seems reasonable that we should hold autonomous agents to, minimally, the same standard we hold humans to. In this paper, we present a framework for autonomous aircraft piloting agents to reason about ethical problems in the context of emergency landings. In particular, we are concerned with ethical problems in which every option is equally unethical with regard to the ethical principles the options violate; and the only distinguishing factor is the likelihood that a plan will violate an ethical principle. We conclude by discussing why, in general, we find an inference-theoretic approach to ethical reasoning to be superior to the model-theoretic approach of prior work.} 
    }
    


  6. Sinclair Gurny, Jason Falvo, and Carlos A. Varela. Aircraft Weight Estimation During Takeoff Using Declarative Machine Learning. In The 39th AIAA/IEEE Digital Avionics Systems Conference (DASC 2020), October 2020. Keyword(s): cyber physical systems, avionics, machine learning, dddas.
    Abstract:
    Aircraft sensors measure physical quantities to help pilots and flight automation systems with situational awareness and decision making. Unfortunately, some important quantities of interest (QoI), e.g. aircraft weight, cannot be directly measured by sensors. As a consequence, accidents can happen, exemplified by Tuninter 1153 and Cessna 172R N4207P, where the airplanes were underweight (not enough fuel) and overweight (6% over maximum gross weight) respectively. Learning models to infer QoI from other aircraft sensor data is thus critical to safety through analytical redundancy. In this paper, we extend PILOTS, our declarative programming language for stream analytics, to learn models from data. We illustrate the supervised machine learning extensions to PILOTS with an example where we use take-off speed profiles under different density altitudes and runway conditions to estimate aircraft weight. Using data we collected from the XPlane flight simulator for a Cessna 172SP, we compare the results of several models on accuracy and timeliness. We also consider ensemble learning to improve the accuracy of weight estimation during takeoff from 94.3% (single model) to 97% (multiple models). Given that the average length of a take-off is 26.75s, this model was able to converge within 10% of the correct weight after 10.7s and converge within 5% after 17.7s. On August 25th, 2014, a Cessna 172R, N4207P, crashed killing the pilot and three passengers. The National Transportation Safety Board (NTSB) report calculated the aircraft to be 1.06 times the maximum gross weight. We simulated the take-off in X-Plane using information from the report. We were able to estimate within 5% error after 8s, which is less than 200ft down the runway, and at the point of take-off, 27s, had an error of 3%. This means that our model could have alerted the pilot of an overweight condition well before the aircraft became airborne, leaving more than 2000ft of runway to come to a stop.

    @InProceedings{gurny-dasc-2020,
    author = {Sinclair Gurny and Jason Falvo and Carlos A. Varela},
    title = {Aircraft Weight Estimation During Takeoff Using Declarative Machine Learning},
    booktitle = {The 39th AIAA/IEEE Digital Avionics Systems Conference (DASC 2020)},
    year = {2020},
    month = {October},
    pdf = {http://wcl.cs.rpi.edu/papers/DASC2020_gurny.pdf},
    keywords = {cyber physical systems, avionics, machine learning, dddas},
    abstract = {Aircraft sensors measure physical quantities to help pilots and flight automation systems with situational awareness and decision making. Unfortunately, some important quantities of interest (QoI), e.g. aircraft weight, cannot be directly measured by sensors. As a consequence, accidents can happen, exemplified by Tuninter 1153 and Cessna 172R N4207P, where the airplanes were underweight (not enough fuel) and overweight (6% over maximum gross weight) respectively. Learning models to infer QoI from other aircraft sensor data is thus critical to safety through analytical redundancy. In this paper, we extend PILOTS, our declarative programming language for stream analytics, to learn models from data. We illustrate the supervised machine learning extensions to PILOTS with an example where we use take-off speed profiles under different density altitudes and runway conditions to estimate aircraft weight. Using data we collected from the XPlane flight simulator for a Cessna 172SP, we compare the results of several models on accuracy and timeliness. We also consider ensemble learning to improve the accuracy of weight estimation during takeoff from 94.3% (single model) to 97% (multiple models). Given that the average length of a take-off is 26.75s, this model was able to converge within 10% of the correct weight after 10.7s and converge within 5% after 17.7s. On August 25th, 2014, a Cessna 172R, N4207P, crashed killing the pilot and three passengers. The National Transportation Safety Board (NTSB) report calculated the aircraft to be 1.06 times the maximum gross weight. We simulated the take-off in X-Plane using information from the report. We were able to estimate within 5% error after 8s, which is less than 200ft down the runway, and at the point of take-off, 27s, had an error of 3%. This means that our model could have alerted the pilot of an overweight condition well before the aircraft became airborne, leaving more than 2000ft of runway to come to a stop.} 
    }
    


  7. Baoluo Meng, Abha Moitra, Andrew W. Crapo, Saswata Paul, Kit Siu, Michael Durling, Daniel Prince, and Heber Herencia-Zapana. Towards Developing Formalized Assurance Cases. In The 39th AIAA/IEEE Digital Avionics Systems Conference (DASC 2020), October 2020. Keyword(s): cyber security, formal verification, assurance case.
    Abstract:
    The ever-increasing complexity of cyber physical systems drives the need for assurance of critical infrastructure and embedded systems. Building assurance cases is a way to increase confidence in systems. In general, the construction of assurance cases is a manual process and the resulting artifacts are not machine analyzable. The High Assurance Systems team at GE Research is developing technology to support generation of formalized assurance cases for systems, which are both humanreadable and machine-analyzable. We have developed a Semantic Application Design Language Assurance Toolkit (SADL-AT) including a semantic model to formalize the Goal Structuring Notation for assurance cases. This paper describes the toolkit SADL-AT and demonstrates the capabilities and effectiveness of SADL-AT by building security and safety assurance case fragments for an unmanned aerial vehicle-based example – a delivery drone.

    @InProceedings{meng-dasc-2020,
    author = {Baoluo Meng and Abha Moitra and Andrew W. Crapo and Saswata Paul and Kit Siu and Michael Durling and Daniel Prince and Heber Herencia-Zapana},
    title = {Towards Developing Formalized Assurance Cases},
    booktitle = {The 39th AIAA/IEEE Digital Avionics Systems Conference (DASC 2020)},
    year = {2020},
    month = {October},
    pdf = {http://wcl.cs.rpi.edu/papers/DASC2020_meng.pdf},
    keywords = {cyber security, formal verification, assurance case},
    abstract = {The ever-increasing complexity of cyber physical systems drives the need for assurance of critical infrastructure and embedded systems. Building assurance cases is a way to increase confidence in systems. In general, the construction of assurance cases is a manual process and the resulting artifacts are not machine analyzable. The High Assurance Systems team at GE Research is developing technology to support generation of formalized assurance cases for systems, which are both humanreadable and machine-analyzable. We have developed a Semantic Application Design Language Assurance Toolkit (SADL-AT) including a semantic model to formalize the Goal Structuring Notation for assurance cases. This paper describes the toolkit SADL-AT and demonstrates the capabilities and effectiveness of SADL-AT by building security and safety assurance case fragments for an unmanned aerial vehicle-based example – a delivery drone.} 
    }
    


  8. Saswata Paul, Fotis Kopsaftopoulos, Stacy Patterson, and Carlos A. Varela. Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms. In Dynamic Data-Driven Application Systems (InfoSymbiotics/DDDAS 2020), Cambridge, MA, October 2020. Keyword(s): cyber physical systems, athena, formal verification, dddas, distributed systems.
    Abstract:
    We present formal progress envelopes to classify a system's operating state space into regions where a formal proof of progress for a distributed algorithm may or may not hold. We also propose an approach for runtime integration of formal methods in the dynamic data-driven applications systems architecture using parameterized proofs. Additionally, we showcase the development of proof libraries for high-level statistical and stochastic reasoning in the Athena proof assistant.

    @InProceedings{paul-dddas-2020,
    author = {Saswata Paul and Fotis Kopsaftopoulos and Stacy Patterson and Carlos A. Varela},
    title = {Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms},
    booktitle = {Dynamic Data-Driven Application Systems (InfoSymbiotics/DDDAS 2020)},
    year = 2020,
    address = {Cambridge, MA},
    month = {October},
    keywords = {cyber physical systems, athena, formal verification, dddas, distributed systems},
    pdf = {http://wcl.cs.rpi.edu/papers/DDDAS2020_paul.pdf},
    abstract = {We present formal progress envelopes to classify a system's operating state space into regions where a formal proof of progress for a distributed algorithm may or may not hold. We also propose an approach for runtime integration of formal methods in the dynamic data-driven applications systems architecture using parameterized proofs. Additionally, we showcase the development of proof libraries for high-level statistical and stochastic reasoning in the Athena proof assistant. } 
    }
    


  9. Saswata Paul, Stacy Patterson, and Carlos A. Varela. Collaborative Situational Awareness for Conflict-Aware Flight Planning. In The 39th AIAA/IEEE Digital Avionics Systems Conference (DASC 2020), October 2020. Keyword(s): cyber physical systems, formal verification, TLA, distributed systems, air traffic management.
    Abstract:
    In autonomous air-traffic management scenarios of the future, manned and unmanned aircraft will be able to safely navigate through the National Airspace System, independent of centralized air-traffic controllers, by sharing critical data necessary for maintaining standard separation with each other. Under such conditions, every aircraft must have sufficient knowledge about other aircraft sharing the airspace to operate safely. In this paper, we specify such a state of knowledge and present a formally verified distributed knowledge propagation protocol, which guarantees that this state will eventually be attained, leading to heightened collaborative situational awareness among the aircraft. We use the TLA$^+$ Specification Language to specify our protocol and some safety-critical correctness properties. We also provide mechanically-verified proofs of the correctness properties, under a set of suitable operating conditions of the system, by using the TLA+ Proof System.

    @InProceedings{paul-dasc-2020,
    author = {Saswata Paul and Stacy Patterson and Carlos A. Varela },
    title = {Collaborative Situational Awareness for Conflict-Aware Flight Planning},
    booktitle = {The 39th AIAA/IEEE Digital Avionics Systems Conference (DASC 2020)},
    year = {2020},
    month = {October},
    pdf = {http://wcl.cs.rpi.edu/papers/DASC2020_paul.pdf},
    keywords = {cyber physical systems, formal verification, TLA, distributed systems, air traffic management},
    abstract = {In autonomous air-traffic management scenarios of the future, manned and unmanned aircraft will be able to safely navigate through the National Airspace System, independent of centralized air-traffic controllers, by sharing critical data necessary for maintaining standard separation with each other. Under such conditions, every aircraft must have sufficient knowledge about other aircraft sharing the airspace to operate safely. In this paper, we specify such a state of knowledge and present a formally verified distributed knowledge propagation protocol, which guarantees that this state will eventually be attained, leading to heightened collaborative situational awareness among the aircraft. We use the TLA$^+$ Specification Language to specify our protocol and some safety-critical correctness properties. We also provide mechanically-verified proofs of the correctness properties, under a set of suitable operating conditions of the system, by using the TLA+ Proof System.} 
    }
    


Miscellaneous
  1. Sinclair Gurny. Learning Models from Avionics Data Streams. Master's thesis, Rensselaer Polytechnic Institute, May 2020. Keyword(s): cyber physical systems, avionics, machine learning, dddas.
    Abstract:
    In aviation, there are many values that are useful for pilots to know that cannot be measured from sensors and require calculation using various charts or other means to accurately estimate. Aircraft take-off distance requires knowing wind speed, pressure altitude, and temperature. However, it is possible for the inputs of these calculations to change during flight, or be calculated incorrectly by mistake, and it would be useful for pilots to know these values in real-time. PILOTS is a programming language for spatio-temporal data stream processing. We have added improved integration for machine learning algorithms as well as a linguistic abstraction for training these models. In data-driven systems, it can be useful to use distributed processes for computation. We have designed a declarative framework for federated learning and the aggregation of results from multiple related models within PILOTS. Furthermore, we built a model using PILOTS that is able to estimate weight in real-time during take-off of a fixed-wing aircraft using data available from the avionics. We evaluated the results of several models on accuracy and timeliness. Data was collected from the flight simulator X-Plane. Accidents such as the fatal crash of Cessna 172R N4207P could have been prevented using the weight estimation methods illustrated.

    @MastersThesis{gurny-msthesis-2020,
    author = {Sinclair Gurny},
    title = {Learning Models from Avionics Data Streams},
    school = {Rensselaer Polytechnic Institute},
    year = 2020,
    month = {May},
    pdf = {http://wcl.cs.rpi.edu/theses/gurny_ms.pdf},
    keywords = {cyber physical systems, avionics, machine learning, dddas},
    abstract = {In aviation, there are many values that are useful for pilots to know that cannot be measured from sensors and require calculation using various charts or other means to accurately estimate. Aircraft take-off distance requires knowing wind speed, pressure altitude, and temperature. However, it is possible for the inputs of these calculations to change during flight, or be calculated incorrectly by mistake, and it would be useful for pilots to know these values in real-time. PILOTS is a programming language for spatio-temporal data stream processing. We have added improved integration for machine learning algorithms as well as a linguistic abstraction for training these models. In data-driven systems, it can be useful to use distributed processes for computation. We have designed a declarative framework for federated learning and the aggregation of results from multiple related models within PILOTS. Furthermore, we built a model using PILOTS that is able to estimate weight in real-time during take-off of a fixed-wing aircraft using data available from the avionics. We evaluated the results of several models on accuracy and timeliness. Data was collected from the flight simulator X-Plane. Accidents such as the fatal crash of Cessna 172R N4207P could have been prevented using the weight estimation methods illustrated.} 
    }
    



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 répertoires 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 gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer 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 détenteur du copyright.




Last modified: Tue Oct 13 12:16:53 2020
Author: pauls4.


This document was translated from BibTEX by bibtex2html