| 41. |
- Kunze, Sebastian, 1990-, et al.
(författare)
-
Generation of Failure Models through Automata Learning
- 2016
-
Ingår i: Proceedings. - Los Alamitos : IEEE Computer Society. - 9781509025718 ; , s. 22-25
-
Konferensbidrag (refereegranskat)abstract
- In the context of the AUTO-CAAS project that deals with model-based testing techniques applied in the automotive domain, we present the preliminary ideas and results of building generalised failure models for non-conformant software components. These models are a necessary building block for our upcoming efforts to detect and analyse failure causes in automotive software built with AUTOSAR components. Concretely, we discuss how to build these generalised failure models using automata learning techniques applied to a guided model-based testing procedure of a failing component. We illustrate our preliminary findings and experiments on a simple integer queue implemented in the C programming language. © 2016 IEEE.
|
|
| 42. |
- Mohaqeqi, Morteza, et al.
(författare)
-
Conformance Testing of Cyber-Physical Systems : A Comparative Study
- 2014
-
Ingår i: Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014). - Berlin : European Association of Software Science and Technology.
-
Konferensbidrag (refereegranskat)abstract
- For systematic and automatic testing of cyber-physical systems, in which a set of test cases is generated based on a formal specification, a number of notions of conformance testing have been proposed. In this paper, we review two existing theories of conformance testing for cyber-physical systems and compare them. We point out their fundamental differences, and prove under which assumptions they coincide. © Automated Verification of Critical Systems 2014.
|
|
| 43. |
- Mohaqeqi, Morteza, et al.
(författare)
-
Sound Test-Suites for Cyber-Physical Systems
- 2016
-
Ingår i: Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering (TASE 2016). - Piscataway : IEEE Computer Society. - 9781509017645 - 9781509017652 ; , s. 42-48
-
Konferensbidrag (refereegranskat)abstract
- Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. © 2016 IEEE.
|
|
| 44. |
- Mohaqeqi, Morteza, et al.
(författare)
-
Towards an Approximate Conformance Relation for Hybrid I/O Automata
- 2016
-
Ingår i: Proceedings of the The First Workshop on Verification and Validation of Cyber-Physical Systems. - Sydney : Open Publishing Association. ; , s. 53-64
-
Konferensbidrag (refereegranskat)abstract
- Several notions of conformance have been proposed for checking the behavior of cyber-physical systems against their hybrid systems models. In this paper, we explore the initial idea of a notion of approximate conformance that allows for comparison of both observable discrete actions and (sampled) continuous trajectories. As such, this notion will consolidate two earlier notions, namely the notion of Hybrid Input-Output Conformance (HIOCO) by M. van Osch and the notion of Hybrid Conformance by H. Abbas and G.E. Fainekos. We prove that our proposed notion of conformance satisfies a semi-transitivity property, which makes it suitable for a step-wise proof of conformance or refinement.
|
|
| 45. |
- Mosses, Peter D., et al.
(författare)
-
Robustness of Behavioral Equivalence on Open Terms
- 2010
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language. This paper investigates preservation of sound equations for several notions of bisimilarity on open terms: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due to Robert de Simone, and hypothesis-preserving (hp-)bisimilarity, due to Arend Rensink. For both fh-bisimilarity and hp-bisimilarity, we prove that arbitrary sound equations on open terms are preserved by all disjoint extensions which do not add labels. We also define slight variations of fh- and hp-bisimilarity such that all sound equations are preserved by arbitrary disjoint extensions. Finally, we give two sets of syntactic criteria (on equations, resp. operational extensions) and prove each of them to be sufficient for preserving ci-bisimilarity.
|
|
| 46. |
|
|
| 47. |
|
|
| 48. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Modeling and Validating Globally Asynchronous Design in Synchronous Frameworks
- 2004
-
Ingår i: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE’04), Volume 1. - Los Alamitos, CA : IEEE Computer Society. - 0769520855 ; , s. 384-389
-
Konferensbidrag (refereegranskat)abstract
- We lay a foundation for modeling and validation of asynchronous designs in a multi-clock synchronous programming model. This allows us to study properties of globally asynchronous systems using synchronous simulation and model-checking toolkits. Our approach can be summarized as automatic transformation of a design consisting of two asynchronously composed synchronous components into a fully synchronous multi-clock model preserving behavioral equivalence. The ultimate goal of this research is to provide the ability to model and build GALS systems in a fully synchronous design framework and deploy it on an asynchronous network preserving all properties of the system proven in the synchronous framework.
|
|
| 49. |
|
|
| 50. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Semantics and expressiveness of ordered SOS
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications. Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules. We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.
|
|
