hh.sePublikationer
Ändra sökning
Länk till posten
Permanent länk

Direktlänk
BETA
Alternativa namn
Publikationer (7 of 7) Visa alla publikationer
Aerts, A., Mousavi, M. R. & Reniers, M. A. (2015). A Tool Prototype for Model-Based Testing of Cyber-Physical Systems. In: Martin Leucker, Camilo Rueda, and Frank D. Valencia (Ed.), Theoretical Aspects of Computing – ICTAC 2015: 12th International Colloquium Cali, Colombia, October 29–31, 2015, Proceedings. Paper presented at The 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Cali, Colombia, October 29-31, 2015 (pp. 563-572). Cham: Springer, 9399
Öppna denna publikation i ny flik eller fönster >>A Tool Prototype for Model-Based Testing of Cyber-Physical Systems
2015 (Engelska)Ingår i: Theoretical Aspects of Computing – ICTAC 2015: 12th International Colloquium Cali, Colombia, October 29–31, 2015, Proceedings / [ed] Martin Leucker, Camilo Rueda, and Frank D. Valencia, Cham: Springer, 2015, Vol. 9399, s. 563-572Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

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

Ort, förlag, år, upplaga, sidor
Cham: Springer, 2015
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9399
Nyckelord
Model-Based Testing, Conformance Testing, Cyber-Physical Systems, Hybrid Systems, Acumen, Matlab
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-29998 (URN)10.1007/978-3-319-25150-9_32 (DOI)000366212700032 ()2-s2.0-84951965541 (Scopus ID)978-3-319-25149-3 (ISBN)978-3-319-25150-9 (ISBN)
Konferens
The 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Cali, Colombia, October 29-31, 2015
Projekt
EFFEMBACAUTO-CAAS
Forskningsfinansiär
ELLIIT - The Linköping‐Lund Initiative on IT and Mobile CommunicationsVetenskapsrådet, 621-2014-5057KK-stiftelsen, 20140302
Anmärkning

M.R. Mousavi has been partially supported by the Swedish Research Council (Vetenskapsrådet) with award number 621-2014-5057 (Effective Model-Based Testing of Parallel Systems) and the Swedish Knowledge Foundation (Stiftelsen för Kunskaps- och Kompetensutveckling) with award number 20140302 (AUTO-CAAS).

Tillgänglig från: 2015-12-09 Skapad: 2015-12-09 Senast uppdaterad: 2018-01-10Bibliografiskt granskad
Cimini, M., Mousavi, M. R., Reniers, M. A. & Gabbay, M. J. (2012). Nominal SOS. In: Ulrich Berger & Michael Mislove (Ed.), Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII): . Paper presented at The 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012), Bath, United Kingdom, 6-9 June, 2012 (pp. 103-116). Amsterdam: Elsevier
Öppna denna publikation i ny flik eller fönster >>Nominal SOS
2012 (Engelska)Ingår i: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII) / [ed] Ulrich Berger & Michael Mislove, Amsterdam: Elsevier, 2012, s. 103-116Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Amsterdam: Elsevier, 2012
Serie
Electronic Notes in Theoretical Computer Science, ISSN 1571-0661 ; 286
Nyckelord
SOS, Nominal SOS, Nominal calculi, λ-calculus, π-calculus
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-20325 (URN)10.1016/j.entcs.2012.08.008 (DOI)2-s2.0-84879218077 (Scopus ID)
Konferens
The 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012), Bath, United Kingdom, 6-9 June, 2012
Tillgänglig från: 2013-01-08 Skapad: 2013-01-08 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
Aceto, L., Cimini, M., Ingólfsdóttir, A., Mousavi, M. R. & Reniers, M. A. (2010). On Rule Formats for Zero and Unit Elements. Eindhoven: Eindhoven University of Technology
Öppna denna publikation i ny flik eller fönster >>On Rule Formats for Zero and Unit Elements
Visa övriga...
2010 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

This paper proposes a rule format for Structural Operational Semantics guaranteeing that certain constants act as left or right zero elements for a set of binary operators. Our design approach is also applied to reformulate an earlier rule format for unit elements developed by some of the authors. Examples of left and right zero, as well as unit, elements from the literature are shown to be checkable using the provided formats.

Ort, förlag, år, upplaga, sidor
Eindhoven: Eindhoven University of Technology, 2010. s. 34
Serie
Computer science report ; 10-03
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-20523 (URN)
Projekt
New Developments in Operational SemanticsMeta-theory of Algebraic Process Theories
Tillgänglig från: 2013-01-09 Skapad: 2013-01-08 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
Mosses, P. D., Mousavi, M. R. & Reniers, M. A. (2010). Robustness of Behavioral Equivalence on Open Terms. Eindhoven: Eindhoven University of Technology
Öppna denna publikation i ny flik eller fönster >>Robustness of Behavioral Equivalence on Open Terms
2010 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Eindhoven: Eindhoven University of Technology, 2010. s. 17
Serie
Computer Science Report ; 10-18
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-20540 (URN)
Tillgänglig från: 2013-01-09 Skapad: 2013-01-08 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
Aceto, L., Cimini, M., Ingólfsdóttir, A., Mousavi, M. R. & Reniers, M. A. (2010). Rule Formats for Distributivity. Eindhoven: Eindhoven University of Technology
Öppna denna publikation i ny flik eller fönster >>Rule Formats for Distributivity
Visa övriga...
2010 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats.

Ort, förlag, år, upplaga, sidor
Eindhoven: Eindhoven University of Technology, 2010. s. 39
Serie
Computer science reports ; 10-16
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-20536 (URN)
Projekt
New Developments in Operational SemanticsMeta-theory of Algebraic Process Theories
Tillgänglig från: 2013-01-09 Skapad: 2013-01-08 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
Aceto, L., Ingólfsdóttir, A., Mousavi, M. R. & Reniers, M. A. (2009). A Rule Format for Unit Elements. Eindhoven: Eindhoven University of Technology
Öppna denna publikation i ny flik eller fönster >>A Rule Format for Unit Elements
2009 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Eindhoven: Eindhoven University of Technology, 2009. s. 13
Serie
Computer science report ; 09-13
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-20510 (URN)
Projekt
The Equational Logic of Parallel ProcessesNew Developments in Operational Semantics
Tillgänglig från: 2013-01-10 Skapad: 2013-01-08 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
Mousavi, M. R., Phillips, I. C. C., Reniers, M. A. & Ulidowski, I. (2007). Semantics and expressiveness of ordered SOS. Eindhoven: Eindhoven University of Technology
Öppna denna publikation i ny flik eller fönster >>Semantics and expressiveness of ordered SOS
2007 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Eindhoven: Eindhoven University of Technology, 2007. s. 37
Serie
Computer science report ; 07-07
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
urn:nbn:se:hh:diva-20492 (URN)
Tillgänglig från: 2013-01-10 Skapad: 2013-01-08 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
Identifikatorer
ORCID-id: ORCID iD iconorcid.org/0000-0002-9283-4074

Sök vidare i DiVA

Visa alla publikationer