Browsing by Author "Lee, I"
Now showing 1 - 3 of 3
- Results Per Page
- Sort Options
Item Open Access Automatic verification of linear controller software(2015 Proceedings of the International Conference on Embedded Software, EMSOFT 2015, 2015-11-04) Pajic, M; Park, J; Lee, I; Pappas, GJ; Sokolsky, O© 2015 IEEE.We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller's state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller's transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.Item Open Access Robust estimation using context-aware filtering(2015 53rd Annual Allerton Conference on Communication, Control, and Computing, Allerton 2015, 2016-04-04) Ivanov, R; Atanasov, N; Pajic, M; Pappas, G.J.; Lee, I© 2015 IEEE.This paper presents the context-aware filter, an estimation technique that incorporates context measurements, in addition to the regular continuous measurements. Context measurements provide binary information about the system's context which is not directly encoded in the state; examples include a robot detecting a nearby building using image processing or a medical device alarming that a vital sign has exceeded a predefined threshold. These measurements can only be received from certain states and can therefore be modeled as a function of the system's current state. We focus on two classes of functions describing the probability of context detection given the current state; these functions capture a wide variety of detections that may occur in practice. We derive the corresponding context-aware filters, a Gaussian Mixture filter and another closed-form filter with a posterior distribution whose moments are derived in the paper. Finally, we evaluate the performance of both classes of functions through simulation of an unmanned ground vehicle.Item Open Access Safety-critical medical device development using the UPP2SF model translation tool(Transactions on Embedded Computing Systems, 2014-01-01) Pajic, M; Jiang, Z; Lee, I; Sokolsky, O; Mangharam, RSoftware-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in themodel-driven design of a pacemaker whosemodel is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems. © 2014 ACM.