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
Oct 14, 2013
Johann Schumann
Kristin Y. Rozier
Thomas Reinbacher
Ole J. Mengshoel
Timmy Mbaya
Corey Ippolito
Abstract
Unmanned aerial systems (UASs) can only be deployed if they can effectively complete their missions and respond to failures and uncertain environmental conditions while maintaining safety with respect to other aircraft as well as humen and property on the ground. In this paper, we design a real-time, on-board system health management (SHM) capability to continuously monitor sensors, software, and hardware components for detection and diagnosis of 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/or software signals; (2) signal analysis, preprocessing, and advanced on- the-fly temporal and Bayesian probabilistic fault diagnosis; (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 due to instrumentation.Our implementation provides a novel approach of combin- ing 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 data from the NASA Swift UAS, an experimental all-electric aircraft.
How to Cite
Schumann, . J., Y. Rozier, K. ., Reinbacher, T. ., J. Mengshoel, . O. ., Mbaya, T. ., & Ippolito, C. . (2013). Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems. Annual Conference of the PHM Society, 5(1). https://doi.org/10.36001/phmconf.2013.v5i1.2275
##plugins.themes.bootstrap3.article.details##
Keywords
Bayesian reasoning, Health Management System, temporal logic, FPGA-hardware, UAS
References
Alur, R., & Henzinger, T. A. (1990). Real-time Logics: Complexity and Expressiveness. In Lics (pp. 390–401). IEEE Computer Society Press.
Barringer, H., et al. (Eds.). (2010). Runtime verification - first international conference, rv 2010, proceedings (Vol. 6418). Springer Verlag.
Basin, D., Klaedtke, F., Mu ̈ller, S., & Pfitzmann, B. (2008). Runtime monitoring of metric first-order temporal properties. In Fsttcs (pp. 49–60).
Basin, D., Klaedtke, F., & Za ̆linescu, E. (2011). Algorithms for monitoring real-time properties. In Rv (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 human-human communication protocols with miscommunication generation and model checking. In Nasa formal methods symposium (Vol. TBD). Springer.
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 Proceedings of the 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-07) (pp. 2443–2449). Hyderabad, India.
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.
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. ECEASST, 46.
Geilen, M. (2003). An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. In Cav (Vol. 2725, pp. 394–406). 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. of the twenty-first national conference on artificial intelligence (p. 143-148). Boston, MA.
Ippolito, C., Espinosa, P., & Weston, A. (2010, April). 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 heterogenous system. In Proc. of the 39th international conference on parallel processing (p. 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-10) (pp. 268–276).
Kozlov, A. V., & Singh, J. P. (1994). A parallel Lauritzen- Spiegelhalter algorithm for probabilistic inference. In Proc. of the 1994 acm/ieee conference on supercom- puting (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.
Li, Z., & D’Ambrosio, B. (1994). Efficient inference in Bayes nets 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). High- throughput Bayesian computing machine with recon-
figurable 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 multi- core computers. In Proc. of the 24th acm international conference on supercomputing (p. 95-104).
Lindsey, A. E., & Pecheur, C. (2004). Simulation-based verification of autonomous controllers via living stone pathfinder. In K. Jensen & A. Podelski (Eds.), Proceedings tacas 2004 (Vol. 2988, pp. 357–371). Springer.
Low, Y., Gonzalez, J., Kyrola, A., Bickson, D., Guestrin, C., & Hellerstein, J. (2010). GraphLab: A new frame- work for parallel machine learning. In Proc. of the 26th annual conference on uncertainty in artificial intelligence (uai-10) (p. 340-349).
Maler, O., Nickovic, D., & Pnueli, A. (2005). Real time temporal logic: Past, present, future. In Formats (Vol. 3829, p. 2-16). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers from bounded-response properties. InCav (Vol. 4590, p. 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 (p. 475-505).
Springer Verlag.
Mengshoel, O. J. (2007). Designing resource-bounded reasoners using Bayesian networks: System health monitoring and diagnosis. In Proceedings of the 18th international workshop on principles of diagnosis (dx-07) (pp. 330–337). Nashville, TN.
Mengshoel, O. J., Chavira, M., Cascio, K., Poll, S., Dar- wiche, A., & Uckun, S. (2010). Probabilistic model- based 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-08) (pp. 1699–1705). Chicago, IL.
Mengshoel, O. J., Roth, D., & Wilkins, D. C. (2011). Port- folios 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.
Musliner, D., Hendler, J., Agrawala, A. K., Durfee, E., Stros- nider, J. K., & Paul, C. J. (1995, January). The challenges of real-time AI. IEEE Computer, 28, 58– 66. Retrieved from citeseer.comp.nus.edu.sg/article/ musliner95challenges.html
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 system (p. 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. San Mateo, CA:Morgan Kaufmann.
Pike, L., Niller, S., & Wegmann, N. (2011). Runtime verification for ultra-critical systems. In Rv (Vol. 7186, pp.310–324). Springer Verlag.
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- 07) (pp. 178–185). Nashville, TN.
Reinbacher, T., Rozier, K. Y., & Schumann, J. (2013). Temporal-logic based runtime observers for system health management of real-time systems.. (under submission)
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-09) (pp. 415–422). Stockholm, Sweden.
Ricks, B. W., & Mengshoel, O. J. (2009b). Methods for probabilistic fault diagnosis: An electrical power sys- tem case study. In Proc. of annual conference of the phm society, 2009 (phm-09). San Diego, CA.
Ricks, B. W., & Mengshoel, O. J. (2010). Diagnosing inter- mittent and persistent faults using static Bayesian networks. In Proc. of the 21st international workshop on principles of diagnosis (dx-10). Portland, OR.
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, 5(2), 163–203.
Rozier, K. Y., & Vardi, M. Y. (2010, March). LTL satisfiability checking. International Journal on Software Tools for Technology Transfer (STTT), 12(2), 123 - 137. Retrieved from http://dx.doi.org/10.1007/s10009 -010-0140-3 doi: DOI10.1007/s10009-010-0140-3
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., Morris, R., Mbaya, T., Mengshoel, O. J., & Darwiche, A. (2011). Report on Bayesian approach for dynamic monitoring of software quality and integration with advanced IVHM engine for ISWHM (Tech. Rep.). USRA/RIACS.
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 sum- products on GPUs through software-managed cache. In Proc. of the 22nd acm international conference on supercomputing (pp. 309–318).
Thati, P., & Ros ̧u, G. (2005). Monitoring algorithms for Metric Temporal Logic specifications. ENTCS, 113, 145–162.
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. of the 19th inter- national symposium on computer architecture and high performance computing (p. 221-228).
Zhang, N. L., & Poole, D. (1996). Exploiting causal independence in Bayesian network inference. Journal of Artificial Intelligence Research, 5, 301-328. Retrieved from citeseer.nj.nec.com/article/zhang96exploiting.html
Zhao, Y., & Rozier, K. Y. (2012). Formal specification and verification of a coordination protocol for an auto- mated air traffic control system. In Proceedings of the 12th international workshop on automated verification of critical systems (avocs 2012) (Vol. 53). European Association of Software Science and Technology.
Zheng, L., & Mengshoel, O. J. (2013, August). Optimizing parallel belief propagation in junction trees using regression. In Proc. of 19th ACM SIGKDD conference on knowledge discovery and data mining (kdd- 13). Chicago, IL.
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-11). Barcelona, Spain.
Barringer, H., et al. (Eds.). (2010). Runtime verification - first international conference, rv 2010, proceedings (Vol. 6418). Springer Verlag.
Basin, D., Klaedtke, F., Mu ̈ller, S., & Pfitzmann, B. (2008). Runtime monitoring of metric first-order temporal properties. In Fsttcs (pp. 49–60).
Basin, D., Klaedtke, F., & Za ̆linescu, E. (2011). Algorithms for monitoring real-time properties. In Rv (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 human-human communication protocols with miscommunication generation and model checking. In Nasa formal methods symposium (Vol. TBD). Springer.
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 Proceedings of the 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-07) (pp. 2443–2449). Hyderabad, India.
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.
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. ECEASST, 46.
Geilen, M. (2003). An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. In Cav (Vol. 2725, pp. 394–406). 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. of the twenty-first national conference on artificial intelligence (p. 143-148). Boston, MA.
Ippolito, C., Espinosa, P., & Weston, A. (2010, April). 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 heterogenous system. In Proc. of the 39th international conference on parallel processing (p. 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-10) (pp. 268–276).
Kozlov, A. V., & Singh, J. P. (1994). A parallel Lauritzen- Spiegelhalter algorithm for probabilistic inference. In Proc. of the 1994 acm/ieee conference on supercom- puting (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.
Li, Z., & D’Ambrosio, B. (1994). Efficient inference in Bayes nets 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). High- throughput Bayesian computing machine with recon-
figurable 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 multi- core computers. In Proc. of the 24th acm international conference on supercomputing (p. 95-104).
Lindsey, A. E., & Pecheur, C. (2004). Simulation-based verification of autonomous controllers via living stone pathfinder. In K. Jensen & A. Podelski (Eds.), Proceedings tacas 2004 (Vol. 2988, pp. 357–371). Springer.
Low, Y., Gonzalez, J., Kyrola, A., Bickson, D., Guestrin, C., & Hellerstein, J. (2010). GraphLab: A new frame- work for parallel machine learning. In Proc. of the 26th annual conference on uncertainty in artificial intelligence (uai-10) (p. 340-349).
Maler, O., Nickovic, D., & Pnueli, A. (2005). Real time temporal logic: Past, present, future. In Formats (Vol. 3829, p. 2-16). Springer Verlag.
Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers from bounded-response properties. InCav (Vol. 4590, p. 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 (p. 475-505).
Springer Verlag.
Mengshoel, O. J. (2007). Designing resource-bounded reasoners using Bayesian networks: System health monitoring and diagnosis. In Proceedings of the 18th international workshop on principles of diagnosis (dx-07) (pp. 330–337). Nashville, TN.
Mengshoel, O. J., Chavira, M., Cascio, K., Poll, S., Dar- wiche, A., & Uckun, S. (2010). Probabilistic model- based 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-08) (pp. 1699–1705). Chicago, IL.
Mengshoel, O. J., Roth, D., & Wilkins, D. C. (2011). Port- folios 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.
Musliner, D., Hendler, J., Agrawala, A. K., Durfee, E., Stros- nider, J. K., & Paul, C. J. (1995, January). The challenges of real-time AI. IEEE Computer, 28, 58– 66. Retrieved from citeseer.comp.nus.edu.sg/article/ musliner95challenges.html
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 system (p. 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. San Mateo, CA:Morgan Kaufmann.
Pike, L., Niller, S., & Wegmann, N. (2011). Runtime verification for ultra-critical systems. In Rv (Vol. 7186, pp.310–324). Springer Verlag.
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- 07) (pp. 178–185). Nashville, TN.
Reinbacher, T., Rozier, K. Y., & Schumann, J. (2013). Temporal-logic based runtime observers for system health management of real-time systems.. (under submission)
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-09) (pp. 415–422). Stockholm, Sweden.
Ricks, B. W., & Mengshoel, O. J. (2009b). Methods for probabilistic fault diagnosis: An electrical power sys- tem case study. In Proc. of annual conference of the phm society, 2009 (phm-09). San Diego, CA.
Ricks, B. W., & Mengshoel, O. J. (2010). Diagnosing inter- mittent and persistent faults using static Bayesian networks. In Proc. of the 21st international workshop on principles of diagnosis (dx-10). Portland, OR.
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, 5(2), 163–203.
Rozier, K. Y., & Vardi, M. Y. (2010, March). LTL satisfiability checking. International Journal on Software Tools for Technology Transfer (STTT), 12(2), 123 - 137. Retrieved from http://dx.doi.org/10.1007/s10009 -010-0140-3 doi: DOI10.1007/s10009-010-0140-3
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., Morris, R., Mbaya, T., Mengshoel, O. J., & Darwiche, A. (2011). Report on Bayesian approach for dynamic monitoring of software quality and integration with advanced IVHM engine for ISWHM (Tech. Rep.). USRA/RIACS.
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 sum- products on GPUs through software-managed cache. In Proc. of the 22nd acm international conference on supercomputing (pp. 309–318).
Thati, P., & Ros ̧u, G. (2005). Monitoring algorithms for Metric Temporal Logic specifications. ENTCS, 113, 145–162.
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. of the 19th inter- national symposium on computer architecture and high performance computing (p. 221-228).
Zhang, N. L., & Poole, D. (1996). Exploiting causal independence in Bayesian network inference. Journal of Artificial Intelligence Research, 5, 301-328. Retrieved from citeseer.nj.nec.com/article/zhang96exploiting.html
Zhao, Y., & Rozier, K. Y. (2012). Formal specification and verification of a coordination protocol for an auto- mated air traffic control system. In Proceedings of the 12th international workshop on automated verification of critical systems (avocs 2012) (Vol. 53). European Association of Software Science and Technology.
Zheng, L., & Mengshoel, O. J. (2013, August). Optimizing parallel belief propagation in junction trees using regression. In Proc. of 19th ACM SIGKDD conference on knowledge discovery and data mining (kdd- 13). Chicago, IL.
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-11). Barcelona, Spain.
Section
Technical Research Papers
The Prognostic and Health Management Society advocates open-access to scientific data and uses a Creative Commons license for publishing and distributing any papers. A Creative Commons license does not relinquish the author’s copyright; rather it allows them to share some of their rights with any member of the public under certain conditions whilst enjoying full legal protection. By submitting an article to the International Conference of the Prognostics and Health Management Society, the authors agree to be bound by the associated terms and conditions including the following:
As the author, you retain the copyright to your Work. By submitting your Work, you are granting anybody the right to copy, distribute and transmit your Work and to adapt your Work with proper attribution under the terms of the Creative Commons Attribution 3.0 United States license. You assign rights to the Prognostics and Health Management Society to publish and disseminate your Work through electronic and print media if it is accepted for publication. A license note citing the Creative Commons Attribution 3.0 United States License as shown below needs to be placed in the footnote on the first page of the article.
First Author et al. This is an open-access article distributed under the terms of the Creative Commons Attribution 3.0 United States License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.