全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...

Querying Parametric Temporal Logic Properties in Model Based Design

Full-Text   Cite this paper   Add to My Lib

Abstract:

One of the advantages of adopting the Model Based Development (MBD) process is that it enables testing and verification at early stages of development. However, it is often desirable to not only verify/falsify certain formal system specifications, but also to automatically explore the properties that the system satisfies. In this work, we present a framework that enables property exploration for Cyber-Physical Systems. Namely, given a parametric specification with multiple parameters, our solution can automatically infer the ranges of parameters for which the property holds/does not hold on the system. In this paper, we consider parametric specifications in Metric Temporal Logic (MTL). Using robust semantics for MTL, the parameter estimation problem can be converted into a Pareto optimization problem for which we can provide an approximate solution by utilizing stochastic optimization methods. We include solutions and algorithms for the exploration and visualization of multi-parameter specifications. The framework is demonstrated on an industrial size, high-fidelity engine model and examples from the related literature.

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133