Search

Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of "lasso"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.

Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this limitation by combining zone-based backward exploration with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. Although the large number of states often prevents successful verification, we show that data variables can be efficienlty handled by the weakest precondition operation. This way our new approach complements existing techniques., Electronic Communications of the EASST, Volume 76: Automated Verification of Critical Systems 2018 (AVoCS 2018)

Software is a continuously evolving product: updates, reconfiguration, new features or just small modifications appear frequently to follow the user needs or to correct errors. However, these modifications might introduce errors or other unexpected consequences. Regression testing is a method being able to verify that the results of the changes are correct, development does not introduce new problems into the system. In order to ensure correctness, regression testing involves the execution of numerous tests usually written manually by the developers. Many techniques try to reduce the testing efforts by reducing the number of regression tests. In this paper we introduce a model-based technique to make regression testing more efficient by focusing on the user-defined properties of the system-under-test.

Cyber-physical systems process a huge amount of data coming from sensors and other information sources and they often have to provide real-time feedback and reaction. Cyber-physical systems are often critical, which means that their failure can lead to serious injuries or even loss of human lives. Ensuring correctness is an important issue, however traditional design-time verification approaches can not be applied due to the complex interaction with the changing environment, the distributed behavior and the intelligent/autonomous solutions. In this paper we present a framework for distributed runtime verification of cyber-physical systems including the solution for executing queries on a distributed model stored on multiple nodes.

Cyber-physical systems are gaining more and more importance even in critical domains, where model-based development and runtime monitoring is becoming an important research area. However, traditional approaches do not always provide the suitable toolset to model their dynamic characteristics. In this paper, we aim to overview and highlight the strengths and limitations of existing runtime and design time modeling techniques that can help runtime monitoring and verification from the viewpoint of dynamic cyber-physical systems. We evaluated instance modeling, metamodeling, and metamodeling with templates, and provided example use-case scenarios for these approaches. We also overview the applicability of SysML in these contexts.

We describe a case of a giant conjunctival nevus presented in a 12-year-old girl with suspicious clinicomorphological appearance. The lesion was noticed by the parents at the age of 3 years as a “fleshy spot” on the bulbar conjunctiva. The lesion remained unchanged until approx. 6 months before recent admission. On slit-lamp examination, a large conjunctival lesion with variegate pigmentation and indistinct margins was detected on the superonasal part of the bulbar conjunctiva of the left eye. Intralesional cysts and vessels were detected with AS-OCT examination. Wide excision and cryotherapy to the scleral bed were performed and amniotic membrane graft was used to restore the ocular surface. Histopathological examination revealed compound type conjunctival nevus and disclosed any sign of malignancy. Although giant conjunctival nevus is a rare entity, precise diagnosis and adequate management are very important as it can be confused with malignant melanoma.