Asset Publisher

On-line fuzzy verification of real time systems and its uncertainty analysis

Doctoral student:
Joaquin Pérez Márquez
Year:
2015
Director(s):
Jaime Jiménez Verde
Description:

Industrial environments demand specification languages expressive enough to model and verify complex scenarios. Such specification requirements demand the flexibility to manage manufacturing event correlations, performance constraints and timing restrictions such as holdups and delays. Under these guidelines, this thesis presents the functional specification language FTL-CFree, a real runtime language that extends temporal logics with fuzzy semantics. Moreover, this language enriches temporal logic expressiveness with random access to past values and fuzzy evolutionary semantics. Given a specific input trace, this interpretation not only aims to measure the degree of truth of an assertion, but also sets how it will evolve in the future, if new trace suffixes are provided. As is usually the case in runtime verification, the language provides for oracle generation, and so, an automatic observable specification can be obtained from high-level requirements. As a result, a real-time monitor is synthesized, and its application in failure detection and quality management systems is an increasingly common practice. Whereas runtime verification provides an online insight into system behavior, the ability to analyze the stationary response during nominal operation is a must for the engineering community. The evaluation outcome of a specification requirement is undoubtedly disturbed by process variability and, therefore, characterizing its statistical properties is an important concern. The semantics of FTL-CFree converts an input scenario into a fuzzy evaluation and, as a result, this can be analyzed by means of random variable algebra. Here, it is possible to demonstrate that an FTL-CFree formula follows a custom probability distribution and, as a result, it can be confirmed that the probability theory is capable of handling randomness in fuzzy measures. Based on this fact, several features can be used, for example, a new methodology to tune the parameters of formulae relating to membership functions and temporal bounds. These parameters can be resolved in an unsupervised manner if certain probabilistic requirements are provided. All aforementioned contributions, the FTL-CFree language, the real-time monitor, the statistical interpretation, and the formula parameterization method are available in the runtime platform PROMIND.