Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userEnvironment Modeling During Model Checking of Cyber-Physical Systems
144
0
0.0
(
0
)
Added by
Zhihao Jiang
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Ensuring the safety and efficacy of Cyber-Physical Systems (CPSs) is challenging due to the large variability of their operating environment. Model checking has been proposed for validation of CPSs, but the models of the environment are either too specific to capture the variability of the environment, or too abstract to provide counter-examples interpretable by experts in the application domain. Domain-specific solutions to this problem require expertise in both formal methods and the application domain, which prevents effective application of model checking in CPSs validation. A domain-independent framework based on timed-automata is proposed for abstraction and refinement of environment models during model checking. The framework maintains an abstraction tree of environment models, which provides interpretable counter-examples while ensuring coverage of environment behaviors. With the framework, experts in the application domain can effectively use model checking without expertise in formal methods.
rate research
Read More
Assuring the correct behavior of cyber-physical systems requires significant modeling effort, particularly during early stages of the engineering and design process when a system is not yet available for testing or verification of proper behavior. A primary motivation for `getting things right in these early design stages is that altering the design is significantly less costly and more effective than when hardware and software have already been developed. Engineering cyber-physical systems requires the construction of several different types of models, each representing a different view, which include stakeholder requirements, system behavior, and the system architecture. Furthermore, each of these models can be represented at different levels of abstraction. Formal reasoning has improved the precision and expanded the available types of analysis in assuring correctness of requirements, behaviors, and architectures. However, each is usually modeled in distinct formalisms and corresponding tools. Currently, this disparity means that a system designer must manually check that the different models are in agreement. Manually editing and checking models is error prone, time consuming, and sensitive to any changes in the design of the models themselves. Wiring diagrams and related theory provide a means for formally organizing these different but related modeling views, resulting in a compositional modeling language for cyber-physical systems. Such a categorical language can make concrete the relationship between different model views, thereby managing complexity, allowing hierarchical decomposition of system models, and formally proving consistency between models.
We present a survey of the saturation method for model-checking pushdown systems.
Cyber-physical systems combine software and physical components. Specification-driven trace-checking tools for CPS usually provide users with a specification language to express the requirements of interest, and an automatic procedure to check whether these requirements hold on the execution traces of a CPS. Although there exist several specification languages for CPS, they are often not sufficiently expressive to allow the specification of complex CPS properties related to the software and the physical components and their interactions. In this paper, we propose (i) the Hybrid Logic of Signals (HLS), a logic-based language that allows the specification of complex CPS requirements, and (ii) ThEodorE, an efficient SMT-based trace-checking procedure. This procedure reduces the problem of checking a CPS requirement over an execution trace, to checking the satisfiability of an SMT formula. We evaluated our contributions by using a representative industrial case study in the satellite domain. We assessed the expressiveness of HLS by considering 212 requirements of our case study. HLS could express all the 212 requirements. We also assessed the applicability of ThEodorE by running the trace-checking procedure for 747 trace-requirement combinations. ThEodorE was able to produce a verdict in 74.5% of the cases. Finally, we compared HLS and ThEodorE with other specification languages and trace-checking tools from the literature. Our results show that, from a practical standpoint, our approach offers a better trade-off between expressiveness and performance.
Demand response (DR) is becoming increasingly important as the volatility on the grid continues to increase. Current DR approaches are completely manual and rule-based or involve deriving first principles based models which are extremely cost and time prohibitive to build. We consider the problem of data-driven end-user DR for large buildings which involves predicting the demand response baseline, evaluating fixed rule based DR strategies and synthesizing DR control actions. We provide a model based control with regression trees algorithm (mbCRT), which allows us to perform closed-loop control for DR strategy synthesis for large commercial buildings. Our data-driven control synthesis algorithm outperforms rule-based DR by $17%$ for a large DoE commercial reference building and leads to a curtailment of $380$kW and over $$45,000$ in savings. Our methods have been integrated into an open source tool called DR-Advisor, which acts as a recommender system for the buildings facilities manager and provides suitable control actions to meet the desired load curtailment while maintaining operations and maximizing the economic reward. DR-Advisor achieves $92.8%$ to $98.9%$ prediction accuracy for 8 buildings on Penns campus. We compare DR-Advisor with other data driven methods and rank $2^{nd}$ on ASHRAEs benchmarking data-set for energy prediction.
Many complex cyber-physical systems can be modeled as heterogeneous components interacting with each other in real-time. We assume that the correctness of each component can be specified as a requirement satisfied by the output signals produced by the component, and that such an output guarantee is expressed in a real-time temporal logic such as Signal Temporal Logic (STL). In this paper, we hypothesize that a large subset of input signals for which the corresponding output signals satisfy the output requirement can also be compactly described using an STL formula that we call the environment assumption. We propose an algorithm to mine such an environment assumption using a supervised learning technique. Essentially, our algorithm treats the environment assumption as a classifier that labels input signals as good if the corresponding output signal satisfies the output requirement, and as bad otherwise. Our learning method simultaneously learns the structure of the STL formula as well as the values of the numeric constants appearing in the formula. To achieve this, we combine a procedure to systematically enumerate candidate Parametric STL (PSTL) formulas, with a decision-tree based approach to learn parameter values. We demonstrate experimental results on real world data from several domains including transportation and health care.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
