| 1. |
- Aceto, Luca, et al.
(författare)
-
A Rule Format for Unit Elements
- 2009
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper offers a meta-theorem for languages with a Structural Operational Semantics (SOS) in the style of Plotkin. Namely, it proposes a generic rule format for SOS guaranteeing that certain constants act as left- or right-unit elements for a set of binary operators. We show the generality of our format by applying it to a wide range of operators from the literature on process calculi.
|
|
| 2. |
- Aceto, Luca, et al.
(författare)
-
Exploiting Algebraic Laws to Improve Mechanized Axiomatizations
- 2013
-
Ingår i: Algebra and Coalgebra in Computer Science. - Berlin : Springer Berlin/Heidelberg. - 9783642402067 - 9783642402050 ; , s. 36-50
-
Konferensbidrag (refereegranskat)abstract
- In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one. © 2013 Springer-Verlag Berlin Heidelberg.
|
|
| 3. |
- Aerts, Arend, et al.
(författare)
-
A Tool Prototype for Model-Based Testing of Cyber-Physical Systems
- 2015
-
Ingår i: Theoretical Aspects of Computing – ICTAC 2015. - Cham : Springer. - 9783319251493 - 9783319251509 ; , s. 563-572
-
Konferensbidrag (refereegranskat)abstract
- We report on a tool prototype for model-based testing of cyber-physical systems. Our starting point is a hybrid-system model specified in a domain-specific language called Acumen. Our prototype tool is implemented in Matlab and covers three stages of model-based testing, namely, test-case generation, test-case execution, and conformance analysis. We have applied our implementation to a number of typical examples of cyber-physical systems in order to analyze its applicability. In this paper, we report on the result of applying the prototype tool on a DC-DC boost converter. © Springer International Publishing Switzerland 2015
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
- 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.
|
|
| 8. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Timed-Gamma and Its Coordination Language
- 2015
-
Ingår i: Nordic Journal of Computing. - Helsinki : University of Helsinki. - 1236-6064. ; 15:2, s. 75-111
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes a theoretical framework for separation of concerns in the formal specification of reactive and real-time systems. This framework consists of the syntax and the semantics of three languages (and all meaningful combinations thereof) that each address a separate concern. The first language, Gamma (a variant of an existing language) is used to define the functionality of a system (by means of a set of basic data transformations). Our additions are a simple language of intervals specifying timing-properties of basic transformations and a language (called Schedules) for specifying the coordination of the basic Gamma transformations. Each of these languages formally models a separate aspect of a system and statements in these languages can be reused, changed or analyzed in their own right. Our key contribution is that we provide a formal framework in which different combinations of aspects have a well-defined semantics.
|
|
