| 101. |
|
|
| 102. |
|
|
| 103. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
Prototyping SOS meta-theory in Maude
- 2006
-
Ingår i: Proceedings of the 2nd Workshop on Structural Operational Semantics (SOS2005, Lisbon, Portugal, July 10, 2005; satellite to ICALP2005). - Amsterdam : Elsevier. ; , s. 135-150
-
Konferensbidrag (refereegranskat)
|
|
| 104. |
- 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.
|
|
| 105. |
- 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.
|
|
| 106. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
SOS formats and meta-theory : 20 years after
- 2007
-
Ingår i: Theoretical Computer Science. - Amsterdam : Elsevier. - 0304-3975 .- 1879-2294. ; 373, s. 238-272
-
Tidskriftsartikel (refereegranskat)abstract
- In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS's) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them. © 2007 Elsevier Ltd. All rights reserved.
|
|
| 107. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Special issue : Software verification and testing
- 2013
-
Ingår i: Innovations in Systems and Software Engineering. - London : Springer London. - 1614-5046 .- 1614-5054. ; 9:2, s. 57-58
-
Tidskriftsartikel (refereegranskat)
|
|
| 108. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Special section on Software Verification and Testing
- 2014
-
Ingår i: Science of Computer Programming. - Amsterdam : Elsevier. - 0167-6423 .- 1872-7964. ; 95, Part 3, s. 273-274
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 109. |
- Mousavi, Mohammad Reza, et al.
(författare)
-
Telling Lies in Process Algebra
- 2018
-
Ingår i: Proceedings. 2018 12th International Symposium on Theoretical Aspects of Software Engineering. - Guangzhou : Institute of Electrical and Electronics Engineers (IEEE). - 9781538673058 - 9781538673065 ; , s. 116-123
-
Konferensbidrag (refereegranskat)abstract
- Epistemic logic is a powerful formalism for reasoning about communication protocols, particularly in the setting with dishonest agents and lies. Operational frameworks such as algebraic process calculi, on the other hand, are powerful formalisms for specifying the narrations of communication protocols. We bridge these two powerful formalisms by presenting a process calculus in which lies can be told. A lie in our framework is a communicated message that is pretended to be a different message (or nothing at all). In our formalism, we focus on what credulous rational agents can infer about a particular run if they know the protocol beforehand. We express the epistemic properties of such specifications in a rich extension of modal mu-calculus with the belief modality and define the semantics of our operational models in the semantic domain of our logic. We formulate and prove criteria that guarantee belief consistency for credulous agents. ©2018 IEEE
|
|
| 110. |
- 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.
|
|
