| 11. |
- Hojjat, Hossein, et al.
(author)
-
A framework for performance evaluation and functional verification in stochastic process algebras
- 2008
-
In: SAC '08. - New York : Association for Computing Machinery (ACM). - 9781595937537 ; , s. 339-346
-
Conference paper (peer-reviewed)abstract
- Despite its relatively short history, a wealth of formalisms exist for algebraic specification of stochastic systems. The goal of this paper is to give such formalisms a unifying framework for performance evaluation and functional verification. To this end, we propose an approach enabling a provably sound transformation from some existing stochastic process algebras, e.g., PEPA and MTIPP, to a generic form in the mCRL2 language. This way, we resolve the semantic differences among different stochastic process algebras themselves, on one hand, and between stochastic process algebras and classic ones, such as mCRL2, on the other hand. From the generic form, one can generate a state space and perform various functional and performance-related analyses, as we illustrate in this paper.
|
|
| 12. |
|
|
| 13. |
- Hojjat, H., et al.
(author)
-
Process algebraic verification of SystemC codes
- 2008
-
In: Application of Concurrency to System Design, 2008. ACSD 2008. 8th International Conference on. - New York : IEEE Press. - 9781424418381 - 9781424418398 ; , s. 62-67
-
Conference paper (peer-reviewed)abstract
- SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC codes by providing a mapping to the process algebra mCRL2. The outstanding advantages of mCRL2 are the support for different data types and a powerful tool-set for model reduction and analysis. A tool is implemented to automatically perform the proposed mapping. This translation enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.
|
|
| 14. |
- Hojjat, H., et al.
(author)
-
Sarir : a Rebeca to mCRL2 translator
- 2007
-
In: Application of Concurrency to System Design, 2007. ACSD 2007. Seventh International Conference on. - Los Alamitos, Calif. : IEEE Computer Society. - 076952902X - 9780769529028 ; , s. 216-220
-
Conference paper (peer-reviewed)abstract
- We describe a translation from Rebeca, an actor-based language, to mCRL2, a process algebra enhanced with data types. The main motivation is to exploit the verification tools and theories developed for mCRL2 in Rebeca. The mapping is applied to several case-studies including the tree identify phase of the IEEE 1394 standard. The results of the experiment show that the minimization tools of mCRL2 can be very effective and the outcome of the present translation outperforms that of the translation to the input language of the Spin model-checker.
|
|
| 15. |
- Mousavi, Mohammad Reza, et al.
(author)
-
A Congruence Rule Format with Universal Quantification
- 2007
-
In: Proceedings of the 4th Workshop on Structural Operational Semantics. - Amsterdam : Elsevier. ; , s. 109-124
-
Conference paper (peer-reviewed)abstract
- We investigate the addition of universal quantification to the meta-theory of Structural Operational Semantics (SOS). We study the syntax and semantics of SOS rules extended with universal quantification and propose a congruence rule format for strong bisimilarity that supports this new feature. © 2007 Elsevier B.V. All rights reserved.
|
|
| 16. |
- Mousavi, Mohammad Reza, et al.
(author)
-
A syntactic commutativity format for SOS
- 2005
-
In: Information Processing Letters. - Amsterdam : Elsevier. - 0020-0190 .- 1872-6119. ; 93:5, s. 217-223
-
Journal article (peer-reviewed)abstract
- Considering operators defined using Structural Operational Semantics (SOS), commutativity axioms are intuitive properties that hold for many of them. Proving this intuition is usually a laborious task, requiring several pages of boring and standard proof. To save this effort, we propose a syntactic SOS format which guarantees commutativity for a set of composition operators.
|
|
| 17. |
- Mousavi, Mohammad Reza, et al.
(author)
-
Notions of bisimulation and congruence formats for SOS with data
- 2005
-
In: Information and Computation. - Amsterdam : Elsevier. - 0890-5401 .- 1090-2651. ; 200, s. 107-147
-
Journal article (peer-reviewed)abstract
- While studying the specification of the operational semantics of different programming languages and formalisms, one can observe the following three facts. First, Plotkin's style of Structural Operational Semantics has become a standard in defining operational semantics. Second, congruence with respect to some notion of bisimilarity is an interesting property for such languages and it is essential in reasoning. Third, there are numerous languages that contain an explicit data part in the state of the operational semantics. The first two facts have resulted in a line of research exploring syntactic formats of operational rules to derive the desired congruence property for free. However, the third point (in combination with the first two) is not sufficiently addressed and there is no standard congruence format for operational semantics with an explicit data state. In this article, we address this problem by studying the implications of the presence of a data state on the notion of bisimilarity. Furthermore, we propose a number of formats for congruence. © 2005 Elsevier Inc. All rights reserved.
|
|
| 18. |
- Mousavi, Mohammad Reza, et al.
(author)
-
On well-foundedness and expressiveness of promoted tyft : being promoted makes a difference
- 2007
-
In: Proceedings of the 3rd Workshop on Structural Operational Semantics. - Amsterdam : Elsevier. ; , s. 45-56
-
Conference paper (peer-reviewed)abstract
- In this paper, we solve two open problems posed by Karen L. Bernstein regarding her promoted tyft format for structured operational semantics. We show that, unlike formats with closed terms as labels, such as the tyft format, the well-foundedness assumption cannot be dropped for the promoted tyft format while preserving the congruence result. We also show that the well-founded promoted tyft format is incomparable to the tyft format with closed terms as labels, i.e., there are transition relations that can be specified by the promoted tyft format but not by the tyft format, and vice versa. © 2007 Elsevier B.V. All rights reserved.
|
|
| 19. |
- Mousavi, Mohammad Reza, et al.
(author)
-
Orthogonal extensions in structural operational semantics
- 2005
-
In: Automata, Languages and Programming. - Heidelberg : Springer. - 9783540275800 - 3540275800 ; , s. 1214-1225
-
Conference paper (peer-reviewed)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).
|
|
| 20. |
|
|
