Marjan Sirjani


  • Associate Professor
    School of Computer Science
    Reykjavik University
    Reykjavik, Iceland

  • School of Electrical and Computer Engineering,
    University of Tehran
    Tehran, Iran

  • Senior Researcher
    School of Computer Science
    Institute for Studies in Theoretical Physics and Mathematics (IPM)
    Tehran, Iran

  • Contact information
    Address:
    School of Computer Science
    Reykjavik University
    Kringlan 1, 103
    Reykjavik, Iceland
    Tel:
    00354 599 6366
    Fax:
    00354 599 6301
    Email:
    m a r j a n [A@T] r u . i s

Open Positions:

Research interests:

  • Formal Methods in Software Engineering
  • Modeling Reactive and Concurrent Systems
  • Object-based Modeling
  • Actor Model
  • Component-based Modeling
  • Formal Verification Methods
  • Model Checking and Reduction Techniques
  • Applying Formal Methods in System Design

Teaching at RU:

Teaching at UT:

Publications:

    2009:
  • M. M. Jaghoori, M. Sirjani, M. R. Mousavi, E. Khamespanah, A. Movaghar, Symmetry and Partial Order Reduction Techniques in Model Checking Rebeca, Acta Informatica, Accepted 2009.
  • N. Razavi, R. Behjati, H. Sabouri, E. Khamespanah, A. Shali, M. Sirjani, Sysfier: Actor-based Formal Verification of SystemC, ACM Transactions on Embedded Computing Systems, Accepted 2009.
  • N. Khakpour, S, Jalili, C. Talcott, M. Sirjani, M. M. Mousavi, PobSAM: Policy-based Managing of Actors in Self-Adaptive Systems, Proceedings of FACS09, LNCS, 2009.
  • B. Pourvatan, M. Sirjani, H. Hojjat, F. Arbab, Automated Analysis of Reo Circuits using Symbolic Execution, Proceedings of FOCLASA09, ENTCS, 2009.
  • N. Khakpour, M. Sirjani and S. Jalili, Formal Analysis of Smart Home Policies using Compositional Verification , Proceedings of ICFI'09, 2009.
  • M.M. Jaghoori, F. de Boer, T. Chotia, and M. Sirjani, Schedulability of asynchronous Real-time concurrent objects, Journal of Logic and Algebraic Programming, Elsevier, Volume 78, Issue 5, pp. 402-416, 2009.
  • H. Hajabdolali Bazzaz, M. Sirjani, R. Khosravi, S. Taheri: Modeling Networking issues of Network-on-chip: a Coloured Petri nets Approach. SimuTools 2009: 22
  • R. Behjati, M. Nili Ahmadabadi, M. Sirjani, Bounded Rational Search for On-the-fly Model Checking of LTL Properties, Proceedings of FSEN´09, Springer LNCS post-proceedings, 2009.

    • 2008:
  • S. Tasharofi, M. Sirjani, Formal Modeling and Conformance Validation for WS-CDL using Reo and CASM, Proceedings of FOCLASA´08, Elsevier ENTCS post-proceedings, 2008.
  • F. Mahdikhani, M. R. Hashemi, M. Sirjani, QoS Aspects in Web Services Compositions, Proceedings of The Fourth IEEE International Symposium on Service-Oriented System Engineering (SOSE 2008), 2008.
  • H. Sabouri, M. Sirjani, Slicing-based Reductions for Rebeca, Proceedings of FACS´08, Elsevier ENTCS post-proceedings, 2008.
  • H. Hojjat, M. R. Mousavi, M. Sirjani, A Framework for Performance Evaluation and Functional Verification in Stochastic Process Algebra, pp. 339-346, ACM SAC 2008.
  • H. Hojjat, M. R. Mousavi, M. Sirjani, Process Algebraic Verification of SystemC Codes, pp. 62-67, IEEE ACSD 2008.
  • R. Behjati, H. Sabouri, N. Razavi, M. Sirjani, An Effecxtive Approach for Model Checking SystemC Designs, pp. 56-61, IEEE ACSD 2008.
  • R. Khosravi, M. Sirjani, N. Asoudeh, S. Sahebi, H. Iravanchi, Modeling and Analysis of Reo Connectors using Alloy, LNCS 5052, pp. 169-183 , Coordination 2008.

    • 2007:
  • M.M. Jaghoori, F. de Boer and M. Sirjani, Task Scheduling in Rebeca, Proceedings of the 19th Nordic Workshop on Programming Theory (NWPT'07), Oslo, Norway, pp. 16-18, October 2007.
  • H. R. Shahriari, M. S. Makarem, M. Sirjani, R. Jalili, A. Movaghar, Vulnerability Analysis of Networks to Detect Multiphase Attacks Using the Actor-based Language Rebeca, Journal of Computers and Electrical Engineering, Accepted 2007.
  • H. Hojjat, H. Nakhost, M. Sirjani., Integrating Module Checking and Deduction in a Formal Proof for the Perlman Spanning Tree Protocol (STP), Journal of Universal Computer Science (J.UCS), vol 13, no. 13, pp. 2076-2104, 2007.
  • N. Hakimipour, N. Razavi, M. Sirjani, Modeling and formal verification of hardware designs. Proceedings of 5th IEEE East-West Design & Test Symposium (EWDTS’07), 2007.
  • C. Talcott, M. Sirjani, S. Ren, Comparing Three Coordination Models: Reo, ARC, and RRD, Proceedings of FOCLASA07, ENTCS, 2007.
  • S. Tasharofi, M. Vakilian, R. Zilouchian Moghaddam, M. Sirjani, Modeling Web Services using Coordination Language Reo, Proceedings of WS-FM07, LNCS, 2007.
  • M. Sirjani, Rebeca: Theory, Applications and Tools, Proceedings of FMCO’06, LNCS 4709, pp. 102 -126, 2007.
  • F. AlaviZadeh, A. Hashemi-Nekoo, M. Sirjani, ReUML: a UML Profile for Modeling and Verification of Reactive Systems, Proceedings of ICSEA’07, 2007.
  • H. Hojjat, M. Sirjani, M. R. Mousavi, J. F. Groote: Sarir, A Rebeca to mCRL2 Translator, Proceedings of. ACSD 2007, IEEE, pp. 216-222, 2007.
  • N. Razavi, M. Sirjani: Compositional Semantics of System-Level Designs Written in SystemC, Proceedings of FSEN 2007, LNCS 4767, pp. 113-128, 2007.
  • M. R. Kakoee, H. Shojaei, H. Ghasemzadeh, Marjan Sirjani, Z. Navabi, A New Approach for Design and Verification of Transaction Level Models, Proceedings of ISCAS 2007, IEEE, pp. 3760-3763, 2007.

    • 2006:
  • C. Baier, M. Sirjani, F. Arbab, J.J. Rutten, Modelin Component Connectors in Reo by Constraint Automata, Science of Computer Programming, Elsevier, Vol. 61, Issue 2, pp. 75-113, July 2006.
  • F. Arbab, M. Sirjani, Preface. Electr. Notes Theor. Comput. Sci., pp.159: 1-2, 2006.
  • M.R. Mousavi, M. Sirjani, F. Arbab, Formal Semantics and Analysis of Component Connectors in Reo., Electr. Notes Theor. Comput. Sci. 154(1).pp. 83-99, 2006.
  • F. Ghassemi, N. Nemat Bakhsh, B. Tork Ladani, M. Sirjani, Specification and Implementation of Multi-Agent Organizations, WEBIST (1) .pp. 447-453, 2006.
  • M. Sirjani, M.M. Jaghoori, C. Baier, F. Arbab, Compositional Semantics of an Actor-Based Language Using Constraint Automata, COORDINATION .pp.281-297, 2006.
  • H. Hojjat, H. Nakhost, M. Sirjani, Formal Verification of the IEEE 802.1D Spanning Tree Protocol Using Extended Rebeca, Electr. Notes Theor. Comput. Sci. 159.pp. 139-154, 2006.
  • F. Ghassemi, S. Tasharofi, M. Sirjani, Automated Mapping of Reo Circuits to Constraint Automata, Electr. Notes Theor. Comput. Sci. 159.pp. 99-115, 2006.
  • M.M. Jaghoori, A. Movaghar, M. Sirjani, Modere: The Model-Checking Engine of Rebeca, ACM Symposium on Applied Computing - Software Verificatin Track, pp. 1810-1815, 2006.

    • 2005:
  • M. Sirjani, F. S. de Boer, A. Movaghar, Modular Verification of a Component-based Actor Language, J.UCS 11, pp. 1695–1717, 2005.
  • M. M. Jaghoori, M. Sirjani, M. R. Mousavi, A. Movaghar, Efficient Symmetry Reduction for an Actor-Based Model. ICDCIT 2005, LNCS 3816, pp. 494-507, 2005.
  • M. Sirjani, , F.S. de Boer, A. Movaghar, A. Shali, Extended Rebeca: A Component-Based Actor Language with Synchronous Message Passing, in Proceedings of ACSD 2005, St. Malo, France, IEEE Computer Society, pp. 212-221, June 2005.
  • M. Sirjani, A. Movaghar, A. Shali, F. S. de Boer: Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models. J. UCS 11(6), pp. 1054-1082, 2005.
  • F. Arbab, C. Baier, F.S. de Boer, J.J.M.M. Rutten and M. Sirjani, Synthesis of Reo Circuits for Implementation of Component-Connector Automata Specifications, Proceedings of the 7th International Conference on Coordination Models and Languages (Coordination 2005), pp. 236-251, 2005.
  • M. Sirjani, A. Movaghar, Integrating Model Checking and Deduction for an Actor-Based Language, Scientia Journal 12(1), pp. 55-65, 2005.
  • N.R. Mehta, N. Medvidovic, M. Sirjani, and F. Arbab, Modeling Behavior in Compositions of Software Architectural Primitives, in Proceedings of ASE 2004, Austria, IEEE Computer Society, pp. 371-374, September 2004.

    • 2004:
  • M. Sirjani, H. SeyedRazi, A. Movaghar, M. M. Jaghouri, S. Forghanizadeh, and M. Mojdeh, Model Checking CSMA/CD Protocol Using an Actor-Based Language, in WSEAS Transactions on Circuit and Systems, Issue 4, Vol. 3, 1052- 1057, June 2004.
  • F. Arbab, C. Baier, J.J.M.M. Rutten and M. Sirjani, Modeling Component Connectors in Reo by Constraint Automata, in Proceedings of FOCLASA'03, Marseille, France, ENTCS 97, pp. 25-46, Elsevier Science, 2004.
  • M. Sirjani. Formal Specification and Verification of Concurrent and Reactive Systems, PhD Thesis, Department of Conputer Engineering, Sharif University of Technology, December 2004.
  • M. Sirjani, Al Movaghar, A. Shali, and F. S. de Boer. Modeling and Verification of Reactive Systems using Rebeca, Fundamenta Informaticae, Vol. 63, Nr. 4, December 2004.
  • M. Sirjani, A. Shali, M.M. Jaghoori, H. Iravanchi, A. Movaghar, A Front-End Tool for Automated Abstraction and Modular Verification of Actor-Based Models, in the International Conference on Application of Concurrency to System Design (ACSD), , June 2004.
  • M. Sirjani, M.M. Jaghoori, S. Forghanizadeh, M. Mojdeh, A. Movaghar. Model Checking CSMA/CD Protocol using an Actor-Based Language, in the Proceedings of the International Conference on Software Engineering, WSEAS, February 2004.

    • 2003:
  • M. Sirjani, A. Movaghar, H. Iravanchi, M.M. Jaghoori and A. Shali, Model Checking in Rebeca, in Proceedings of The 2003 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA' 03), Las Vegas, USA, CSREA Press, pp. 1819-1822, June 2003.
  • M. Sirjani, A. Movaghar, H. Iravanchi, M.M. Jaghoori and A. Shali, Model Checking Rebeca by SMV, in Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS'03), University of Southampton, April 2003.

    • 2002:
  • M. Sirjani and A. Movaghar, Simulation in Rebeca, in Proceedings of the 2002 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA' 02), Las Vegas, USA, CSREA Press, pp.923-926, June 2002.
  • M. Sirjani, A. Movaghar, An Object-Based Model for Agents, in Proceedings of Workshop on Agents for Information Management (EURASIA’02), Shiraz, Iran, Austrian Computer Society, October 2002.
  • S.H. Mirian-Hosseinabadi and M. Sirjani, A Calculus for Real-Time Specification Statements, in Proceedings of the Workshop on Recent Progress in Computers and Communication (EURASIA’02), Shiraz, Iran, Austrian Computer Society, October 2002.
  • M. Sirjani and A. Movaghar, Simulation in Rebeca, in Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS'02), University of Birmingham, April 2002.

    • 2001:
  • M. Sirjani, A. Movaghar, and M.R. Mousavi, Compositional Verification of an Actor-Based Model for Reactive Systems, in Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS'01), Oxford University, April 2001.

Technical Reports:

  • M. Sirjani, F.S. de Boer, A. Movaghar and A. Shali, Extending Rebeca with Synchronous Messages and Reusable Components, SEN-R0505, CWI, Amsterdam, March 2005.
  • F. Arbab, C. Baier, F.S. de Boer, J.J.M.M. Rutten and M. Sirjani, Synthesis of Reo Circuits For Implementation Of Component-Connector Automata Specifications, SEN-R0412, CWI, Amsterdam, August 2004.
  • M.R. Mousavi, M. Sirjani, and F. Arbab, Specification and Verification of Component Connectors, Technical report 04-15, Department of Computer Science, Eindhoven University of Technology, Eindhoven, June 2004.
  • N.R. Mehta, M. Sirjani and F. Arbab, Effective Modeling of Software Architectural Assemblies Using Constraint Automata, SEN-R0309, CWI, Amsterdam, October 2003.
  • F. Arbab, C. Baier, J.J.M.M. Rutten and M. Sirjani, Modeling Component Connectors in Reo by Constraint Automata, SEN-R0304, CWI, Amsterdam, July 2003.
  • M. Sirjani and A. Movaghar, An Actor-Based Model for Reactive Systems: Rebeca, Computer Engineering Dept, Sharif University of Technology, Tehran, 2001.
  • M. Sirjani, A. Movaghar, H. Iravanchi, M.M. Jaghoori and A. Shali, Model Checking Rebeca by SMV, Computer Engineering Dept, Sharif University of Technology, http://mehr.sharif.edu /~msirjani, October 2002, (in Persian).
  • M. Sirjani, Formal Specification and Verification of Concurrent and Real-time Systems, Computer Engineering Dept., Sharif University of Technology, July 2000 (in Persian).
  • M. Sirjani, Lecture Notes used for teaching Programming Languages Analysis and Design, 1999 (in Persian).
  • M. Sirjani, Lecture Notes used for teaching Software Engineering, 1995 (in Persian).
Last Updated at March 3, 2008 by Mohammad-Javad Izadi