| 11. |
- Aerts, Arend, et al.
(författare)
-
Model-Based Testing of Cyber-Physical Systems
- 2016
-
Ingår i: Cyber-Physical Systems. - Saint Louis : Elsevier. - 9780128038017 ; , s. 287-304
-
Bokkapitel (refereegranskat)abstract
- Cyber-physical systems (CPSs) are the result of the integration of connected computer systems with the physical world. They feature complex interactions that go beyond traditional communication schemes and protocols in computer systems. One distinguished feature of such complex interactions is the tight coupling between discrete and continuous interactions, captured by hybrid system models.Due to the complexity of CPSs, providing rigorous and model-based analysis methods and tools for verifying correctness of such systems is of the utmost importance. Model-based testing (MBT) is one such verification technique that can be used for checking the conformance of an implementation of a system to its specification (model).In this chapter, we first review the main concepts and techniques in MBT. Subsequently, we review the most common modeling formalisms for CPSs, with focus on hybrid system models. Subsequently, we provide a brief overview of conformance relations and conformance testing techniques for CPSs. © 2017 Elsevier Inc. All rights reserved.
|
|
| 12. |
- Cimini, Matteo, et al.
(författare)
-
Nominal SOS
- 2012
-
Ingår i: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). - Amsterdam : Elsevier. ; , s. 103-116
-
Konferensbidrag (refereegranskat)abstract
- Plotkin’s style of Structural Operational Semantics (SOS) has become a de facto standard in giving operational semantics to formalisms and process calculi. In many such formalisms and calculi, the concepts of names, variables and binders are essential ingredients. In this paper, we propose a formal framework for dealing with names in SOS. The framework is based on the Nominal Logic of Gabbay and Pitts and hence is called Nominal SOS. We define nominal bisimilarity, an adaptation of the notion of bisimilarity that is aware of binding. We provide evidence of the expressiveness of the framework by formulating the early π-calculus and Abramsky’s lazy λ-calculus within Nominal SOS. For both calculi we establish the operational correspondence with the original calculi. Moreover, in the context of the π-calculus, we prove that nominal bisimilarity coincides with Sangiorgi’s open bisimilarity and in the context of the λ-calculus we prove that nominal bisimilarity coincides with Abramsky’s applicative bisimilarity. © 2012 Elsevier B.V.
|
|
| 13. |
- Cranen, Sjoerd, et al.
(författare)
-
A rule format for associativity
- 2008
-
Ingår i: CONCUR 2008 - Concurrency Theory. - Berlin : Springer Berlin/Heidelberg. - 9783540853602 - 9783540853619 - 354085360X ; , s. 447-461
-
Konferensbidrag (refereegranskat)abstract
- We propose a rule format that guarantees associativity of binary operators with respect to all notions of behavioral equivalence that are defined in terms of (im)possibility of transitions, e.g., the notions below strong bisimilarity in van Glabbeek's spectrum. The initial format is a subset of the De Simone format. We show that all trivial generalizations of our format are bound for failure. We further extend the format in a few directions and illustrate its application to several formalisms in the literature. A subset of the format is studied to obtain associativity with respect to graph isomorphism.
|
|
| 14. |
- Goorden, Martijn, et al.
(författare)
-
Compositional coordinator synthesis of extended finite automata
- 2021
-
Ingår i: Discrete Event Dynamic Systems: Theory and Applications. - : Springer Science and Business Media LLC. - 0924-6703 .- 1573-7594. ; 31:3, s. 317-348
-
Tidskriftsartikel (refereegranskat)abstract
- To avoid the state-space explosion problem, a set of supervisors may be synthesized using divide and conquer strategies, like modular or multilevel synthesis. Unfortunately, these supervisors may be conflicting, meaning that even though they are individually non-blocking, they are together blocking. Abstraction-based compositional nonblocking verification of extended finite automata provides means to verify whether a set of models is nonblocking. In case of a blocking system, a coordinator can be synthesized to resolve the blocking. This paper presents a framework for compositional coordinator synthesis for discrete-event systems modeled as extended finite automata. The framework allows for synthesis of a coordinator on the abstracted system in case compositional verification identifies the system to be blocking. As the abstracted system may use notions not present in the original model, like renamed events, the synthesized coordinator is refined such that it will be nonblocking, controllable, and maximally permissive for the original system. For each abstraction, it is shown how this refinement can be performed. It turns out that for the presented set of abstractions the coordinator refinement is straightforward.
|
|
| 15. |
- Goorden, Martijn, et al.
(författare)
-
Model properties for efficient synthesis of nonblocking modular supervisors
- 2021
-
Ingår i: Control Engineering Practice. - : Elsevier BV. - 0967-0661. ; 112
-
Tidskriftsartikel (refereegranskat)abstract
- Supervisory control theory provides means to synthesize supervisors for systems with discrete-event behavior from models of the uncontrolled plant and of the control requirements. The applicability of supervisory control theory often fails due to a lack of scalability of the algorithms. This paper proposes a format for the requirements and a method to ensure that the crucial properties of controllability and nonblockingness directly hold, thus avoiding the most computationally expensive parts of synthesis. The method consists of creating a control problem dependency graph and verifying whether it is acyclic. Vertices of the graph are modular plant components, and edges are derived from the requirements. In case of a cyclic graph, potential blocking issues can be localized, so that the original control problem can be reduced to only synthesizing supervisors for smaller partial control problems. The strength of the method is illustrated on two case studies: a production line and a roadway tunnel.
|
|
| 16. |
- 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.
|
|
| 17. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
Orthogonal extensions in structural operational semantics
- 2005
-
Ingår i: Automata, Languages and Programming. - Heidelberg : Springer. - 9783540275800 - 3540275800 ; , s. 1214-1225
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we give novel and more liberal notions of operationaland equational conservativity for language extensions. We motivatethese notions by showing their practical application in existing formalisms.Based on our notions, we formulate and prove meta-theoremsthat establish conservative extensions for languages defined using StructuralOperational Semantics (SOS).
|
|
| 18. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
Semantics and expressiveness of ordered SOS
- 2009
-
Ingår i: Information and Computation. - Maryland Heights, USA : Academic Press. - 0890-5401 .- 1090-2651. ; 207:2, s. 85-119
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 19. |
- 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.
|
|
| 20. |
- Rashidinejad, Aida, et al.
(författare)
-
Non-blocking Supervisory Control of Timed Automata using Forcible Events
- 2020
-
Ingår i: IFAC-PapersOnLine. - : Elsevier BV. - 2405-8963. ; 53:4, s. 356-362
-
Konferensbidrag (refereegranskat)abstract
- Real-valued clocks make the state space of timed automata (TA) infinite. Conventional supervisory control synthesis techniques are only applicable to finite automata (FA). Therefore, to synthesize a supervisor for TA using conventional techniques, an abstraction of TA to FA is required. For many applications, the abstraction of real-time values results in an explosion in the finite state space. This paper presents a supervisory control synthesis technique applied directly to TA without any abstraction. The plant is given as a TA with a set of uncontrollable events and a set of forcible events that may preempt the passage of time. To obtain a non-blocking controlled system, a synthesis algorithm is proposed that delivers a supervisor (also as a TA) avoiding the blocking states. The algorithm works by (iteratively) strengthening the guards of edges labeled by controllable events and invariants of locations where time progress can be preempted by forcible events.
|
|
