-
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.}
}
-
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."
}
-
Elkin Cruz-Camacho,
Saswata Paul,
Fotis Kopsaftopoulos,
and Carlos A. Varela.
Towards Provably Correct Probabilistic Flight Systems.
In Frederica Darema,
Erik Blasch,
Sai Ravela,
and Alex Aved, editors,
Dynamic Data Driven Application Systems,
Cham,
pages 236-244,
2020.
Springer International Publishing.
ISBN: 978-3-030-61725-7.
Keyword(s): formal verification,
runtime verification.
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 {\$}{\$}{\backslash}tau {\$}{\$}-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 Agda proof assistant, from which formally proven sentinel code can be generated. |
@InProceedings{cruz-dddas-2020,
author="Cruz-Camacho, Elkin and Paul, Saswata and Kopsaftopoulos, Fotis and Varela, Carlos A.",
editor="Darema, Frederica and Blasch, Erik and Ravela, Sai and Aved, Alex",
title="Towards Provably Correct Probabilistic Flight Systems",
booktitle="Dynamic Data Driven Application Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="236--244",
keywords = {formal verification, runtime verification},
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 {\$}{\$}{\backslash}tau {\$}{\$}-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 Agda proof assistant, from which formally proven sentinel code can be generated.",
isbn="978-3-030-61725-7",
url = {http://wcl.cs.rpi.edu/papers/DDDAS2020_Cruz.pdf}
}
-
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}
}
-
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.}
}
-
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.}
}
-
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.}
}
-
Saswata Paul,
Fotis Kopsaftopoulos,
Stacy Patterson,
and Carlos A. Varela.
Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms.
In Frederica Darema,
Erik Blasch,
Sai Ravela,
and Alex Aved, editors,
Dynamic Data Driven Application Systems,
Cham,
pages 245-252,
2020.
Springer International Publishing.
ISBN: 978-3-030-61725-7.
Keyword(s): dddas,
formal verification,
Athena,
distributed systems,
distributed computing,
air traffic management,
cyber physical systems,
runtime verification.
Abstract: |
This work presents formal progress envelopes applied to flight systems for distinctly classifying a system's state space into regions where a formal proof of progress for a distributed algorithm holds or does not hold. It also presents an approach for runtime integration of formal methods in the dynamic data-driven applications systems (DDDAS) architecture using parameterized proofs. Finally, it showcases the development of reusable parameterized proof libraries for high-level statistical and stochastic reasoning in the Athena proof assistant and demonstrates their use with a progress proof for the Paxos distributed consensus protocol. |
@InProceedings{paul-dddas-2020,
author="Paul, Saswata and Kopsaftopoulos, Fotis and Patterson, Stacy and Varela, Carlos A.",
editor="Darema, Frederica and Blasch, Erik and Ravela, Sai and Aved, Alex",
title="Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms",
booktitle="Dynamic Data Driven Application Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="245--252",
keywords = {dddas, formal verification, Athena, distributed systems, distributed computing, air traffic management, cyber physical systems, runtime verification},
abstract="This work presents formal progress envelopes applied to flight systems for distinctly classifying a system's state space into regions where a formal proof of progress for a distributed algorithm holds or does not hold. It also presents an approach for runtime integration of formal methods in the dynamic data-driven applications systems (DDDAS) architecture using parameterized proofs. Finally, it showcases the development of reusable parameterized proof libraries for high-level statistical and stochastic reasoning in the Athena proof assistant and demonstrates their use with a progress proof for the Paxos distributed consensus protocol.",
isbn="978-3-030-61725-7",
url = {http://wcl.cs.rpi.edu/papers/DDDAS2020_paul.pdf}
}
-
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,
distributed computing,
air traffic management,
knowledge.
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, distributed computing, air traffic management, knowledge},
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.}
}