Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems
##plugins.themes.bootstrap3.article.main##
##plugins.themes.bootstrap3.article.sidebar##
Published
Nov 1, 2020
Johann Schumann
Kristin Y. Rozier
Thomas Reinbacher
Ole J. Mengshoel
Timmy Mbaya
Corey Ippolito
Abstract
For unmanned aerial systems (UAS) to be successfully deployed and integrated within the national airspace, it is imperative that they possess the capability to effectively complete their missions without compromising the safety of other aircraft, as well as persons and property on the ground. This necessity creates a natural requirement for UAS that can respond
to uncertain environmental conditions and emergent failures in real-time, with robustness and resilience close enough to those of manned systems. We introduce a system that meets this requirement with the design of a real-time onboard system health management (SHM) capability to continuously monitor sensors, software, and hardware components. This system can detect and diagnose failures and violations of safety or performance rules during the flight of a UAS. Our approach to SHM is three-pronged, providing: (1) real-time monitoring of sensor and software signals; (2) signal analysis, preprocessing, and advanced on-the-fly temporal and Bayesian probabilistic fault diagnosis; and (3) an unobtrusive, lightweight, read-only, low-power realization using Field Programmable Gate Arrays (FPGAs) that avoids overburdening limited computing resources or costly re-certification of flight software. We call this approach rt-R2U2, a name derived from its requirements. Our implementation provides a novel approach of combining modular building blocks, integrating responsive runtime monitoring of temporal logic system safety requirements with model-based diagnosis and Bayesian network-based probabilistic analysis. We demonstrate this approach using actual flight data from the
NASA Swift UAS.
##plugins.themes.bootstrap3.article.details##
Keywords
fault detection, FPGA, Linear Temporal Logic, Bayesian network
References
Alur, R., & Henzinger, T. A. (1990). Real-time Logics: Complexity and Expressiveness. In LICS (pp. 390–401). IEEE Computer Society Press.
Austin, T. M. (1999). DIVA: A reliable substrate for deep submicron microarchitecture design. In Micro (pp.196–207). IEEE Computer Society Press.
Barr, M. (2013). Bookout vs. Toyota, 2005 Camry L4 Software Analysis. (redacted) Retrieved from http://www.safetyresearch.net/Library/BarrSlides FINAL SCRUBBED.pdf
Basin, D., Klaedtke, F., M¨uller, S., & Pfitzmann, B. (2008). Runtime Monitoring of Metric First-order Temporal Properties. In FSTTCS (pp. 49–60).
Basin, D., Klaedtke, F., & Z˘alinescu, E. (2011). Algorithms for monitoring real-time properties. In Proc. 11th International Conference on Runtime Verification (RV’11) (Vol. 7186, pp. 260–275). Springer Verlag.
Bauer, A., Leucker, M., & Schallhart, C. (2010). Comparing LTL semantics for Runtime Verification. J. Log. and Comput., 20(3), 651–674.
Bekkerman, R., Bilenko, M., & Langford, J. (Eds.). (2011). Scaling up machine learning: Parallel and distributed approaches. Cambridge University Press.
Bellman, R. (1958). On a routing problem. Quarterly of Applied Mathematics, 16, 87–90.
Bolton, M., & Bass, E. (2013). Evaluating humanhuman communication protocols with miscommunication generation and model checking. In Proc. NASA Formal Methods Symposium (Vol. 7871, pp. 42–68). Springer Verlag.
Bonakdarpour, B., & Smolka, S. A. (Eds.). (2014). Proc. Runtime Verification, Fifth International Conference, RV’14 (Vol. 8734). Springer Verlag.
Br¨orkens, M., & M¨oller, M. (2002). Dynamic event generation for runtime checking using the JDI. Electronic Notes in Theoretical Computer Science, 70(4), 21 - 35.
Brown, R., & Hwang, P. (1997). Introduction to Random Signals and Applied Kalman Filtering (3rd ed.). John Wiley & Sons.
Chavira, M., & Darwiche, A. (2005). Compiling Bayesian networks with local structure. In Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI) (pp. 1306–1312).
Chavira, M., & Darwiche, A. (2007). Compiling Bayesian networks using variable elimination. In Proc. of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI) (pp. 2443–2449).
Chenard, J.-S. (2011). Hardware-based temporal logic checkers for the debugging of digital integrated circuits [Dissertation]. McGill University Montreal, Canada.
Choi, A., Darwiche, A., Zheng, L., & Mengshoel, O. J. (2011). A tutorial on Bayesian networks for system health management. In A. Srivastava & J. Han (Eds.), Data mining in systems health management: Detection, diagnostics, and prognostics. Chapman and Hall/CRC Press.
Darwiche, A. (2001). Recursive conditioning. Artificial Intelligence, 126(1-2), 5-41.
Darwiche, A. (2003). A differential approach to inference in Bayesian networks. Journal of the ACM, 50(3), 280–305.
Darwiche, A. (2009). Modeling and reasoning with Bayesian networks. Cambridge, UK: Cambridge University Press.
Dawid, A. P. (1992). Applications of a general propagation algorithm for probabilistic expert systems. Statistics and Computing, 2, 25–36.
Divakaran, S., D’Souza, D., & Mohan, M. R. (2010). Conflict-tolerant real-time specifications in Metric Temporal Logic. In Time (p. 35-42). IEEE Computer Society Press.
Drusinsky, D. (2003). Monitoring temporal rules combined with time series. In CAV (Vol. 2725, pp. 114–118). Springer Verlag. Federal Aviation Administration. (2013). Federal Aviation Regulation §91.
Gan, X., Dubrovin, J., & Heljanko, K. (2011). A symbolic model checking approach to verifying satellite onboard software. Electronic Communications of the EASST, 46, 1–15.
Geilen, M. (2003). An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. In Proc. Computer Aided Verification (CAV) (Vol. 2725, pp. 394–406). Springer Verlag.
Geist, J., Rozier, K. Y., & Schumann, J. (2014). Runtime Observer Pairs and Bayesian Network Reasoners Onboard FPGAs: Flight-Certifiable System Health Management for Embedded Systems. In Proc. 14th International Conference on Runtime Verification (RV’14) (Vol. 8734, pp. 215–230). Springer-Verlag.
Havelund, K. (2008). Runtime Verification of C Programs. In TestCom/FATES (pp. 7–22). Springer Verlag.
Huang, C., & Darwiche, A. (1994). Inference in belief networks: A procedural guide. International Journal of Approximate Reasoning, 15(3), 225-263.
Huang, J., Chavira, M., & Darwiche, A. (2006). Solving MAP exactly by searching on compiled arithmetic circuits. In Proc. 21st National Conference on Artificial Intelligence (pp. 143–148).
Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., & Rosu, G. (2014). ROSRV: Runtime Verification for Robots. In Proc. 14th International Conference on Runtime Verification (RV’14) (Vol. 8734, pp. 247–254). Springer Verlag.
Ippolito, C., Espinosa, P., & Weston, A. (2010). Swift UAS: An electric UAS research platform for green aviation at NASA Ames Research Center. In CAFE EAS IV.
Jensen, F. V., Lauritzen, S. L., & Olesen, K. G. (1990). Bayesian updating in causal probabilistic networks by local computations. SIAM Journal on Computing, 4, 269–282.
Jeon, H., Xia, Y., & Prasanna, V. K. (2010). Parallel exact Inference on a CPU-GPGPU heterogeneous System. In Proc. of the 39th International Conference on Parallel Processing (pp. 61–70).
Johnson, D. (2007). Raptors Arrive at Kadena. Retrieved from http://www.af.mil/news/story.asp?storyID=123041567
Kask, K., Dechter, R., & Gelfand, A. (2010). BEEM: bucket elimination with external memory. In Proc. of the 26th Annual Conference on Uncertainty in Artificial Intelligence (UAI) (pp. 268–276).
Koller, D., & Friedman, N. (2009). Probabilistic graphical methods: Principles and techniques. MIT Press.
Kozlov, A. V., & Singh, J. P. (1994). A parallel Lauritzen- Spiegelhalter algorithm for probabilistic inference. In Proc. of the 1994 ACM/IEEE Conference on Supercomputing (pp. 320–329).
Kulesza, Z., & Tylman, W. (2006). Implementation of Bayesian network in FPGA circuit. In Mixdes (p. 711-715). IEEE Computer Society Press.
Lauritzen, S. L., & Spiegelhalter, D. J. (1988). Local computations with probabilities on graphical structures and their application to expert systems. Journal of the Royal Statistical Society, 50(2), 157–224.
Legay, A., & Bensalem, S. (Eds.). (2013). Proc. Runtime Verification, Fourth International Conference, RV’13 (Vol.8174). Springer Verlag.
Li, Z.,& D’Ambrosio, B. (1994). Efficient inference in Bayesnets as a combinatorial optimization problem. International Journal of Approximate Reasoning, 11(1), 55–81.
Lichtenstein, O., Pnueli, A., & Zuck, L. (1985). The glory of the past. In Logics of programs (Vol. 193, p. 196-218). Springer Verlag.
Lin, M., Lebedev, I., & Wawrzynek, J. (2010). Highthroughput Bayesian computing machine with reconfigurable hardware. In FPGA (pp. 73–82). ACM Press.
Linderman, M. D., Bruggner, R., Athalye, V., Meng, T. H., Asadi, N. B., & Nolan, G. P. (2010). High-throughput Bayesian network learning using heterogeneous Multicore Computers. In Proc. of the 24th ACM International Conference on Supercomputing (pp. 95–104).
Lindsey, A. E., & Pecheur, C. (2004). Simulation-based verification of autonomous controllers via Livingstone Pathfinder. In Proc. TACAS 2004 (Vol. 2988, pp. 357–371). Springer Verlag.
Low, Y., Gonzalez, J., Kyrola, A., Bickson, D., Guestrin, C., & Hellerstein, J. (2010). GraphLab: A new framework for parallel machine learning. In Proc. of the 26th Annual Conference on Uncertainty in Artificial Intelligence (UAI) (p. 340-349).
Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P. O., Serbanuta, T. F., & Rosu, G. (2014). RV-Monitor: Efficient parametric runtime verification with simultaneous properties. In Proc. 14th International Conference on Runtime Verification (RV’14). (Vol. 8734, pp. 285–300). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2005). Real Time Temporal Logic: Past, Present, Future. In FORMATS (Vol. 3829, pp. 2–16). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers from bounded-response properties. In Proc. CAV (Vol. 4590, pp. 95–107). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2008). Checking temporal properties of discrete, timed and continuous behaviors. In Pillars of Comp. Science (pp. 475–505). Springer Verlag.
Mengshoel, O. J. (2007). Designing resource-bounded reasoners using Bayesian networks: System health monitoring and diagnosis. In Proc. 18th International Workshop on Principles of Diagnosis (DX) (pp. 330–337).
Mengshoel, O. J., Chavira, M., Cascio, K., Poll, S., Darwiche, A., & Uckun, S. (2010). Probabilistic modelbased diagnosis: An electrical power system case study. IEEE Trans. on Systems, Man and Cybernetics, Part A: Systems and Humans, 40(5), 874–885.
Mengshoel, O. J., Darwiche, A., Cascio, K., Chavira, M., Poll, S., & Uckun, S. (2008). Diagnosing faults in electrical power systems of spacecraft and aircraft. In Proc. of the Twentieth Innovative Applications of Artificial Intelligence Conference (IAAI) (pp. 1699–1705). Chicago, IL.
Mengshoel, O. J., Roth, D., & Wilkins, D. C. (2011). Portfolios in stochastic local search: Efficiently computing most probable explanations in Bayesian networks. Journal of Automated Reasoning, 46(2), 103–160.
Mengshoel, O. J., Wilkins, D. C., & Roth, D. (2011). Initialization and restart in stochastic local search: Computing a most probable explanation in Bayesian networks. IEEE Transactions on Knowledge and Data Engineering, 23(2), 235–247.
Musliner, D., Hendler, J., Agrawala, A. K., Durfee, E., Strosnider, J. K., & Paul, C. J. (1995). The challenges of real-time AI. IEEE Computer, 28, 58–66.
Namasivayam, V. K., & Prasanna, V. K. (2006). Scalable parallel implementation of exact inference in Bayesian networks. In Proc. of the 12th International Conference on Parallel and Distributed Systems (pp. 143–150).
Park, J. D., & Darwiche, A. (2004). Complexity results and approximation strategies for MAP explanations. Journal of Artificial Intelligence Research (JAIR), 21, 101-133.
Pasricha, R., & Sharma, S. (2009). An FPGA-based design of fixed-point Kalman filter. ICGST International Journal on Digital Signal Processing, DSP, 9, 1–9.
Pearl, J. (1988). Probabilistic reasoning in intelligent systems: Networks of plausible inference. Morgan Kaufmann.
Pearl, J. (2000). Causality : models, reasoning, and inference. Cambridge University Press.
Pellizzoni, R., Meredith, P., Caccamo, M., & Rosu, G. (2008). Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. RTSS, 481-491.
Pike, L., Goodloe, A., Morisset, R., & Niller, S. (2010). Copilot: A Hard Real-Time Runtime Monitor. In Proc. 10th International Conference on Runtime Verification (RV’10) (Vol. 6418, pp. 345–359). Springer Verlag.
Pike, L., Niller, S., & Wegmann, N. (2011). Runtime verification for ultra-critical systems. In Proc. 14th International Conference on Runtime Verification (RV’14) (Vol. 7186, pp. 310–324). Springer Verlag.
Pnueli, A. (1977). The temporal Logic of Programs. In Proc. 18th Annual Conference on Foundations of Computer Science (FOCS’77) (pp. 46–57). IEEE Computer Society Press.
Poll, S., Patterson-Hine, A., Camisa, J., Garcia, D., Hall, D., Lee, C.& Koutsoukos, X. (2007). Advanced Diagnostics and Prognostics Testbed. In Proc. of the 18th International Workshop on Principles of Diagnosis (DX) (pp. 178–185).
Qadeer, S., & Tasiran, S. (Eds.). (2012). Proc. Runtime Verification, Third International Conference, RV’12 (Vol. 7687). Springer Verlag.
Reinbacher, T. (2013). Analysis of embedded real-time systems at runtime Dissertation. Vienna University of Technology Vienna, Austria.
Reinbacher, T., Rozier, K. Y., & Schumann, J. (2014). Temporal-logic based runtime observer pairs for system health management of real-time systems. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Vol. 8413, pp. 357–372). Springer-Verlag.
Ricks, B., & Mengshoel, O. J. (2014). Diagnosis for uncertain, dynamic and hybrid domains using Bayesian Networks and Arithmetic Circuits. International Journal of Approximate Reasoning, 55(5), 1207–1234.
Ricks, B. W., & Mengshoel, O. J. (2009a). The diagnostic challenge competition: Probabilistic techniques for fault diagnosis in electrical power systems. In Proc. of the 20th International Workshop on Principles of Diagnosis (DX) (pp. 415–422).
Ricks, B.W., & Mengshoel, O. J. (2009b). Methods for probabilistic fault diagnosis: An electrical power system case study. In Proc. Annual Conference of the PHM Society (PHM’2009).
Ricks, B. W., & Mengshoel, O. J. (2010). Diagnosing intermittent and persistent faults using static Bayesian networks. In Proc. of the 21st International Workshop on Principles of Diagnosis (DX).
Ristic, B., Arulampalam, S., & Gordon, N. (2004). Beyond the Kalman Filter: Particle Filters for Tracking Applications.Artech House.
Rozier, K. Y. (2011). Linear Temporal Logic Symbolic Model Checking. Computer Science Review Journal, 5(2), 163–203.
Rozier, K. Y., & Vardi, M. Y. (2010). LTL satisfiability checking. International Journal on Software Tools for Technology Transfer (STTT), 12(2), 123 - 137.
RTCA. (2012). DO-178C/ED-12C: Software considerations in airborne systems and equipment certification. Retrieved from http://www.rtca.org
Schumann, J., Mbaya, T., Mengshoel, O. J., Pipatsrisawat, K., Srivastava, A., Choi, A., & Darwiche, A. (2013). Software Health Management with Bayesian Networks. Innovations in Systems and Software Engineering, 9(2), 1–22.
Schumann, J., Mengshoel, O. J., & Mbaya, T. (2011). Integrated software and sensor health management for small spacecraft. In Proc. of the 2011 IEEE Fourth International Conference on Space Mission Challenges for Information Technology (pp. 77–84).
Schumann, J., Roychoudhury, I., & Kulkarni, C. (2015). Diagnostic reasoning using prognostic information for unmanned aerial systems. In Proc. Annual Conference of the PHM Society (PHM’2015) PHM (under review).
Schumann, J., Rozier, K. Y., Reinbacher, T., Mengshoel, O. J., Mbaya, T., & Ippolito, C. (2013). Towards Realtime, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems. In Proc. Annual Conference of the Prognostics and Health Management Society (PHM’2013).
Shenoy, P. P. (1989). A valuation-based language for expert systems. International Journal of Approximate Reasoning, 3(5), 383 – 411.
Silberstein, M., Schuster, A., Geiger, D., Patney, A., & Owens, J. D. (2008). Efficient computation of sumproducts on GPUs through software-managed cache. In Proc. of the 22nd ACM International Conference on Supercomputing (pp. 309–318).
Srivastava, A. N., & Schumann, J. (2013). Software Health Management: a necessity for safety critical systems. Innovations in Systems and Software Engineering, 9(1), 219–233.
Thati, P., & Ros¸u, G. (2005). Monitoring algorithms for Metric Temporal Logic specifications. ENTCS, 113, 145–162.
Tsai, J. J., Fang, K. Y., Chen, H. Y., & Bi, Y. (1990). A noninterference monitoring and replay mechanism for real-time software testing and debugging. Transactions on Software Engineering, 16, 897–916.
Watterson, C., & Heffernan, D. (2007). Runtime verification and monitoring of embedded systems. IET Software, 1(5), 172-179.
Whittle, J., & Schumann, J. (2004, December). Automating the implementation of Kalman filter algorithms. ACM Transactions on Mathematical Software, 30(4), 434–453.
Xia, Y., & Prasanna, V. K. (2007). Node level primitives for parallel exact inference. In Proc. 19th International Symposium on Computer Architecture and High Performance Computing (pp. 221–228).
Ye, B., & Zhang, Y. (2009). Improved FPGA implementation of particle filter for radar tracking applications. In 2nd Asian-Pacific Conference on Synthetic Aperture Radar (APSAR) (pp. 943–946).
Zhang, N. L., & Poole, D. (1996). Exploiting causal independence in Bayesian network inference. Journal of Artificial Intelligence Research, 5, 301-328.
Zhao, Y., & Rozier, K. Y. (2012). Formal specification and verification of a coordination protocol for an automated air traffic control system. In Proc. 12th International Workshop on automated Verification of critical Systems (AVoCS 2012) (Vol. 53). European Association of Software Science and Technology.
Zhao, Y., & Rozier, K. Y. (2014a). Formal specification and verification of a coordination protocol for an automated air traffic control system. Science of Computer Programming Journal, 96(3), 337-353.
Zhao, Y., & Rozier, K. Y. (2014b). Probabilistic model checking for comparative analysis of automated air traffic control systems. In Proc. 33rd IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2014) (pp. 690–695). IEEE/ACM.
Zheng, L., & Mengshoel, O. J. (2013). Optimizing parallel belief propagation in junction trees using regression. In Proc. of 19th ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD-13).
Zheng, L., Mengshoel, O. J.,&Chong, J. (2011). Belief propagation by message passing in junction trees: Computing each message faster using GPU parallelization. In Proc. of the 27th Conference in Uncertainty in Artificial Intelligence (UAI).
Austin, T. M. (1999). DIVA: A reliable substrate for deep submicron microarchitecture design. In Micro (pp.196–207). IEEE Computer Society Press.
Barr, M. (2013). Bookout vs. Toyota, 2005 Camry L4 Software Analysis. (redacted) Retrieved from http://www.safetyresearch.net/Library/BarrSlides FINAL SCRUBBED.pdf
Basin, D., Klaedtke, F., M¨uller, S., & Pfitzmann, B. (2008). Runtime Monitoring of Metric First-order Temporal Properties. In FSTTCS (pp. 49–60).
Basin, D., Klaedtke, F., & Z˘alinescu, E. (2011). Algorithms for monitoring real-time properties. In Proc. 11th International Conference on Runtime Verification (RV’11) (Vol. 7186, pp. 260–275). Springer Verlag.
Bauer, A., Leucker, M., & Schallhart, C. (2010). Comparing LTL semantics for Runtime Verification. J. Log. and Comput., 20(3), 651–674.
Bekkerman, R., Bilenko, M., & Langford, J. (Eds.). (2011). Scaling up machine learning: Parallel and distributed approaches. Cambridge University Press.
Bellman, R. (1958). On a routing problem. Quarterly of Applied Mathematics, 16, 87–90.
Bolton, M., & Bass, E. (2013). Evaluating humanhuman communication protocols with miscommunication generation and model checking. In Proc. NASA Formal Methods Symposium (Vol. 7871, pp. 42–68). Springer Verlag.
Bonakdarpour, B., & Smolka, S. A. (Eds.). (2014). Proc. Runtime Verification, Fifth International Conference, RV’14 (Vol. 8734). Springer Verlag.
Br¨orkens, M., & M¨oller, M. (2002). Dynamic event generation for runtime checking using the JDI. Electronic Notes in Theoretical Computer Science, 70(4), 21 - 35.
Brown, R., & Hwang, P. (1997). Introduction to Random Signals and Applied Kalman Filtering (3rd ed.). John Wiley & Sons.
Chavira, M., & Darwiche, A. (2005). Compiling Bayesian networks with local structure. In Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI) (pp. 1306–1312).
Chavira, M., & Darwiche, A. (2007). Compiling Bayesian networks using variable elimination. In Proc. of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI) (pp. 2443–2449).
Chenard, J.-S. (2011). Hardware-based temporal logic checkers for the debugging of digital integrated circuits [Dissertation]. McGill University Montreal, Canada.
Choi, A., Darwiche, A., Zheng, L., & Mengshoel, O. J. (2011). A tutorial on Bayesian networks for system health management. In A. Srivastava & J. Han (Eds.), Data mining in systems health management: Detection, diagnostics, and prognostics. Chapman and Hall/CRC Press.
Darwiche, A. (2001). Recursive conditioning. Artificial Intelligence, 126(1-2), 5-41.
Darwiche, A. (2003). A differential approach to inference in Bayesian networks. Journal of the ACM, 50(3), 280–305.
Darwiche, A. (2009). Modeling and reasoning with Bayesian networks. Cambridge, UK: Cambridge University Press.
Dawid, A. P. (1992). Applications of a general propagation algorithm for probabilistic expert systems. Statistics and Computing, 2, 25–36.
Divakaran, S., D’Souza, D., & Mohan, M. R. (2010). Conflict-tolerant real-time specifications in Metric Temporal Logic. In Time (p. 35-42). IEEE Computer Society Press.
Drusinsky, D. (2003). Monitoring temporal rules combined with time series. In CAV (Vol. 2725, pp. 114–118). Springer Verlag. Federal Aviation Administration. (2013). Federal Aviation Regulation §91.
Gan, X., Dubrovin, J., & Heljanko, K. (2011). A symbolic model checking approach to verifying satellite onboard software. Electronic Communications of the EASST, 46, 1–15.
Geilen, M. (2003). An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. In Proc. Computer Aided Verification (CAV) (Vol. 2725, pp. 394–406). Springer Verlag.
Geist, J., Rozier, K. Y., & Schumann, J. (2014). Runtime Observer Pairs and Bayesian Network Reasoners Onboard FPGAs: Flight-Certifiable System Health Management for Embedded Systems. In Proc. 14th International Conference on Runtime Verification (RV’14) (Vol. 8734, pp. 215–230). Springer-Verlag.
Havelund, K. (2008). Runtime Verification of C Programs. In TestCom/FATES (pp. 7–22). Springer Verlag.
Huang, C., & Darwiche, A. (1994). Inference in belief networks: A procedural guide. International Journal of Approximate Reasoning, 15(3), 225-263.
Huang, J., Chavira, M., & Darwiche, A. (2006). Solving MAP exactly by searching on compiled arithmetic circuits. In Proc. 21st National Conference on Artificial Intelligence (pp. 143–148).
Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., & Rosu, G. (2014). ROSRV: Runtime Verification for Robots. In Proc. 14th International Conference on Runtime Verification (RV’14) (Vol. 8734, pp. 247–254). Springer Verlag.
Ippolito, C., Espinosa, P., & Weston, A. (2010). Swift UAS: An electric UAS research platform for green aviation at NASA Ames Research Center. In CAFE EAS IV.
Jensen, F. V., Lauritzen, S. L., & Olesen, K. G. (1990). Bayesian updating in causal probabilistic networks by local computations. SIAM Journal on Computing, 4, 269–282.
Jeon, H., Xia, Y., & Prasanna, V. K. (2010). Parallel exact Inference on a CPU-GPGPU heterogeneous System. In Proc. of the 39th International Conference on Parallel Processing (pp. 61–70).
Johnson, D. (2007). Raptors Arrive at Kadena. Retrieved from http://www.af.mil/news/story.asp?storyID=123041567
Kask, K., Dechter, R., & Gelfand, A. (2010). BEEM: bucket elimination with external memory. In Proc. of the 26th Annual Conference on Uncertainty in Artificial Intelligence (UAI) (pp. 268–276).
Koller, D., & Friedman, N. (2009). Probabilistic graphical methods: Principles and techniques. MIT Press.
Kozlov, A. V., & Singh, J. P. (1994). A parallel Lauritzen- Spiegelhalter algorithm for probabilistic inference. In Proc. of the 1994 ACM/IEEE Conference on Supercomputing (pp. 320–329).
Kulesza, Z., & Tylman, W. (2006). Implementation of Bayesian network in FPGA circuit. In Mixdes (p. 711-715). IEEE Computer Society Press.
Lauritzen, S. L., & Spiegelhalter, D. J. (1988). Local computations with probabilities on graphical structures and their application to expert systems. Journal of the Royal Statistical Society, 50(2), 157–224.
Legay, A., & Bensalem, S. (Eds.). (2013). Proc. Runtime Verification, Fourth International Conference, RV’13 (Vol.8174). Springer Verlag.
Li, Z.,& D’Ambrosio, B. (1994). Efficient inference in Bayesnets as a combinatorial optimization problem. International Journal of Approximate Reasoning, 11(1), 55–81.
Lichtenstein, O., Pnueli, A., & Zuck, L. (1985). The glory of the past. In Logics of programs (Vol. 193, p. 196-218). Springer Verlag.
Lin, M., Lebedev, I., & Wawrzynek, J. (2010). Highthroughput Bayesian computing machine with reconfigurable hardware. In FPGA (pp. 73–82). ACM Press.
Linderman, M. D., Bruggner, R., Athalye, V., Meng, T. H., Asadi, N. B., & Nolan, G. P. (2010). High-throughput Bayesian network learning using heterogeneous Multicore Computers. In Proc. of the 24th ACM International Conference on Supercomputing (pp. 95–104).
Lindsey, A. E., & Pecheur, C. (2004). Simulation-based verification of autonomous controllers via Livingstone Pathfinder. In Proc. TACAS 2004 (Vol. 2988, pp. 357–371). Springer Verlag.
Low, Y., Gonzalez, J., Kyrola, A., Bickson, D., Guestrin, C., & Hellerstein, J. (2010). GraphLab: A new framework for parallel machine learning. In Proc. of the 26th Annual Conference on Uncertainty in Artificial Intelligence (UAI) (p. 340-349).
Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P. O., Serbanuta, T. F., & Rosu, G. (2014). RV-Monitor: Efficient parametric runtime verification with simultaneous properties. In Proc. 14th International Conference on Runtime Verification (RV’14). (Vol. 8734, pp. 285–300). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2005). Real Time Temporal Logic: Past, Present, Future. In FORMATS (Vol. 3829, pp. 2–16). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers from bounded-response properties. In Proc. CAV (Vol. 4590, pp. 95–107). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2008). Checking temporal properties of discrete, timed and continuous behaviors. In Pillars of Comp. Science (pp. 475–505). Springer Verlag.
Mengshoel, O. J. (2007). Designing resource-bounded reasoners using Bayesian networks: System health monitoring and diagnosis. In Proc. 18th International Workshop on Principles of Diagnosis (DX) (pp. 330–337).
Mengshoel, O. J., Chavira, M., Cascio, K., Poll, S., Darwiche, A., & Uckun, S. (2010). Probabilistic modelbased diagnosis: An electrical power system case study. IEEE Trans. on Systems, Man and Cybernetics, Part A: Systems and Humans, 40(5), 874–885.
Mengshoel, O. J., Darwiche, A., Cascio, K., Chavira, M., Poll, S., & Uckun, S. (2008). Diagnosing faults in electrical power systems of spacecraft and aircraft. In Proc. of the Twentieth Innovative Applications of Artificial Intelligence Conference (IAAI) (pp. 1699–1705). Chicago, IL.
Mengshoel, O. J., Roth, D., & Wilkins, D. C. (2011). Portfolios in stochastic local search: Efficiently computing most probable explanations in Bayesian networks. Journal of Automated Reasoning, 46(2), 103–160.
Mengshoel, O. J., Wilkins, D. C., & Roth, D. (2011). Initialization and restart in stochastic local search: Computing a most probable explanation in Bayesian networks. IEEE Transactions on Knowledge and Data Engineering, 23(2), 235–247.
Musliner, D., Hendler, J., Agrawala, A. K., Durfee, E., Strosnider, J. K., & Paul, C. J. (1995). The challenges of real-time AI. IEEE Computer, 28, 58–66.
Namasivayam, V. K., & Prasanna, V. K. (2006). Scalable parallel implementation of exact inference in Bayesian networks. In Proc. of the 12th International Conference on Parallel and Distributed Systems (pp. 143–150).
Park, J. D., & Darwiche, A. (2004). Complexity results and approximation strategies for MAP explanations. Journal of Artificial Intelligence Research (JAIR), 21, 101-133.
Pasricha, R., & Sharma, S. (2009). An FPGA-based design of fixed-point Kalman filter. ICGST International Journal on Digital Signal Processing, DSP, 9, 1–9.
Pearl, J. (1988). Probabilistic reasoning in intelligent systems: Networks of plausible inference. Morgan Kaufmann.
Pearl, J. (2000). Causality : models, reasoning, and inference. Cambridge University Press.
Pellizzoni, R., Meredith, P., Caccamo, M., & Rosu, G. (2008). Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. RTSS, 481-491.
Pike, L., Goodloe, A., Morisset, R., & Niller, S. (2010). Copilot: A Hard Real-Time Runtime Monitor. In Proc. 10th International Conference on Runtime Verification (RV’10) (Vol. 6418, pp. 345–359). Springer Verlag.
Pike, L., Niller, S., & Wegmann, N. (2011). Runtime verification for ultra-critical systems. In Proc. 14th International Conference on Runtime Verification (RV’14) (Vol. 7186, pp. 310–324). Springer Verlag.
Pnueli, A. (1977). The temporal Logic of Programs. In Proc. 18th Annual Conference on Foundations of Computer Science (FOCS’77) (pp. 46–57). IEEE Computer Society Press.
Poll, S., Patterson-Hine, A., Camisa, J., Garcia, D., Hall, D., Lee, C.& Koutsoukos, X. (2007). Advanced Diagnostics and Prognostics Testbed. In Proc. of the 18th International Workshop on Principles of Diagnosis (DX) (pp. 178–185).
Qadeer, S., & Tasiran, S. (Eds.). (2012). Proc. Runtime Verification, Third International Conference, RV’12 (Vol. 7687). Springer Verlag.
Reinbacher, T. (2013). Analysis of embedded real-time systems at runtime Dissertation. Vienna University of Technology Vienna, Austria.
Reinbacher, T., Rozier, K. Y., & Schumann, J. (2014). Temporal-logic based runtime observer pairs for system health management of real-time systems. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Vol. 8413, pp. 357–372). Springer-Verlag.
Ricks, B., & Mengshoel, O. J. (2014). Diagnosis for uncertain, dynamic and hybrid domains using Bayesian Networks and Arithmetic Circuits. International Journal of Approximate Reasoning, 55(5), 1207–1234.
Ricks, B. W., & Mengshoel, O. J. (2009a). The diagnostic challenge competition: Probabilistic techniques for fault diagnosis in electrical power systems. In Proc. of the 20th International Workshop on Principles of Diagnosis (DX) (pp. 415–422).
Ricks, B.W., & Mengshoel, O. J. (2009b). Methods for probabilistic fault diagnosis: An electrical power system case study. In Proc. Annual Conference of the PHM Society (PHM’2009).
Ricks, B. W., & Mengshoel, O. J. (2010). Diagnosing intermittent and persistent faults using static Bayesian networks. In Proc. of the 21st International Workshop on Principles of Diagnosis (DX).
Ristic, B., Arulampalam, S., & Gordon, N. (2004). Beyond the Kalman Filter: Particle Filters for Tracking Applications.Artech House.
Rozier, K. Y. (2011). Linear Temporal Logic Symbolic Model Checking. Computer Science Review Journal, 5(2), 163–203.
Rozier, K. Y., & Vardi, M. Y. (2010). LTL satisfiability checking. International Journal on Software Tools for Technology Transfer (STTT), 12(2), 123 - 137.
RTCA. (2012). DO-178C/ED-12C: Software considerations in airborne systems and equipment certification. Retrieved from http://www.rtca.org
Schumann, J., Mbaya, T., Mengshoel, O. J., Pipatsrisawat, K., Srivastava, A., Choi, A., & Darwiche, A. (2013). Software Health Management with Bayesian Networks. Innovations in Systems and Software Engineering, 9(2), 1–22.
Schumann, J., Mengshoel, O. J., & Mbaya, T. (2011). Integrated software and sensor health management for small spacecraft. In Proc. of the 2011 IEEE Fourth International Conference on Space Mission Challenges for Information Technology (pp. 77–84).
Schumann, J., Roychoudhury, I., & Kulkarni, C. (2015). Diagnostic reasoning using prognostic information for unmanned aerial systems. In Proc. Annual Conference of the PHM Society (PHM’2015) PHM (under review).
Schumann, J., Rozier, K. Y., Reinbacher, T., Mengshoel, O. J., Mbaya, T., & Ippolito, C. (2013). Towards Realtime, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems. In Proc. Annual Conference of the Prognostics and Health Management Society (PHM’2013).
Shenoy, P. P. (1989). A valuation-based language for expert systems. International Journal of Approximate Reasoning, 3(5), 383 – 411.
Silberstein, M., Schuster, A., Geiger, D., Patney, A., & Owens, J. D. (2008). Efficient computation of sumproducts on GPUs through software-managed cache. In Proc. of the 22nd ACM International Conference on Supercomputing (pp. 309–318).
Srivastava, A. N., & Schumann, J. (2013). Software Health Management: a necessity for safety critical systems. Innovations in Systems and Software Engineering, 9(1), 219–233.
Thati, P., & Ros¸u, G. (2005). Monitoring algorithms for Metric Temporal Logic specifications. ENTCS, 113, 145–162.
Tsai, J. J., Fang, K. Y., Chen, H. Y., & Bi, Y. (1990). A noninterference monitoring and replay mechanism for real-time software testing and debugging. Transactions on Software Engineering, 16, 897–916.
Watterson, C., & Heffernan, D. (2007). Runtime verification and monitoring of embedded systems. IET Software, 1(5), 172-179.
Whittle, J., & Schumann, J. (2004, December). Automating the implementation of Kalman filter algorithms. ACM Transactions on Mathematical Software, 30(4), 434–453.
Xia, Y., & Prasanna, V. K. (2007). Node level primitives for parallel exact inference. In Proc. 19th International Symposium on Computer Architecture and High Performance Computing (pp. 221–228).
Ye, B., & Zhang, Y. (2009). Improved FPGA implementation of particle filter for radar tracking applications. In 2nd Asian-Pacific Conference on Synthetic Aperture Radar (APSAR) (pp. 943–946).
Zhang, N. L., & Poole, D. (1996). Exploiting causal independence in Bayesian network inference. Journal of Artificial Intelligence Research, 5, 301-328.
Zhao, Y., & Rozier, K. Y. (2012). Formal specification and verification of a coordination protocol for an automated air traffic control system. In Proc. 12th International Workshop on automated Verification of critical Systems (AVoCS 2012) (Vol. 53). European Association of Software Science and Technology.
Zhao, Y., & Rozier, K. Y. (2014a). Formal specification and verification of a coordination protocol for an automated air traffic control system. Science of Computer Programming Journal, 96(3), 337-353.
Zhao, Y., & Rozier, K. Y. (2014b). Probabilistic model checking for comparative analysis of automated air traffic control systems. In Proc. 33rd IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2014) (pp. 690–695). IEEE/ACM.
Zheng, L., & Mengshoel, O. J. (2013). Optimizing parallel belief propagation in junction trees using regression. In Proc. of 19th ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD-13).
Zheng, L., Mengshoel, O. J.,&Chong, J. (2011). Belief propagation by message passing in junction trees: Computing each message faster using GPU parallelization. In Proc. of the 27th Conference in Uncertainty in Artificial Intelligence (UAI).
Section
Technical Papers