Loading...
Search for:
sirjani--m
0.129 seconds
Total 21479 records
Integrating module checking and deduction in a formal proof for the perlman Spanning Tree Protocol (STP)
, Article Journal of Universal Computer Science ; Volume 13, Issue 13 , 2007 , Pages 2076-2104 ; 0958695X (ISSN) ; Nakhost, H ; Sirjani, M ; Sharif University of Technology
2007
Abstract
In the IEEE 802.1D standard for the Media Access Control layer (MAC layer) bridges, there is an STP (Spanning Tree Protocol) definition, based on the algorithm that was proposed by Radia Perlman. In this paper, we give a formal proof for correctness of the STP algorithm by showing that finally a single node is selected as the root of the tree and the loops are eliminated correctly. We use formal inductive reasoning to establish these requirements. In order to ensure that the bridges behave correctly regardless of the topology of the surrounding bridges and LANs, the Rebeca, modular verification techniques are applied. These techniques are shown to be efficiently applicable in model checking...
Modeling component connectors in reo by constraint automata: (Extended abstract)
, Article Proceedings of FOCLASA 2003, the Foundations of Coordination Languages and Software Architectures, a satellite event of CONCUR 2003, Marseille, 2 September 2003 through 2 September 2003 ; Volume 97 , 2004 , Pages 25-46 ; 15710661 (ISSN) ; Baier, C ; Rutten, J ; Sirjani, M ; Sharif University of Technology
2004
Abstract
Reo is an exogenous coordination language for compositional construction of component connectors based on a calculus of channels. Building automated tools to address such concerns as equivalence or containment of the behavior of two given connectors, verification of the behavior of a connector, etc. requires an operational semantic model suitable for model checking. In this paper we introduce constraint automata and propose them as a semantic model for Reo. © 2004 Elsevier B.V. All rights reserved
VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance
, Article International Journal on Software Tools for Technology Transfer ; Volume 22, Issue 5 , 30 June , 2020 , Pages 617-633 ; Khamespanah, E ; Gharib, M ; Sirjani, M ; Movaghar, A ; Sharif University of Technology
Springer Science and Business Media Deutschland GmbH
2020
Abstract
Vehicular ad hoc networks have attracted the attention of many researchers during the last years due to the emergence of autonomous vehicles and safety concerns. Most of the frameworks which are proposed for the modeling and analysis VANET applications make use of simulation techniques. Due to the high level of concurrency in these applications, simulation results do not guarantee the correct behavior of the system and more accurate analysis techniques are required. In this paper, we have developed a framework to provide model checking facilities for the analysis of VANET applications. To this end, an actor-based modeling language, Rebeca, is used which is equipped with a variety of model...
A front-end tool for automated abstraction and modular verification of actor-based models
, Article Proceedings - Fourth International Conference on Application of Concurrency to System Design, ACSD 2004, Hamilton, Ont., 16 June 2004 through 18 June 2004 ; 2004 , Pages 145-148 ; 0769520774 (ISBN); 9780769520773 (ISBN) ; Shali, A ; Jaghoori, M. M ; Iravanchi, H ; Movaghar, A ; Sharif University of Technology
2004
Abstract
Actor-based modeling is known to be an appropriate approach for representing concurrent and distributed systems. Rebeca is an actor-based language with a formal foundation, based on an operational interpretation of the actor model. We develop a front-end tool for translating a subset of Rebeca to SMV in order to model check Rebeca models. Automated modular verification and abstraction techniques are supported by the tool
Modeling behavior in compositions of software architectural primitives
, Article Proceedings - 19th International Conference on Automated Software Engineering, ASE 2004, Linz, 20 September 2004 through 24 September 2004 ; 2004 , Pages 371-374 ; 0769521312 (ISBN); 9780769521312 (ISBN) ; Medvidovic, N ; Sirjani, M ; Arbab, F ; Sharif University of Technology
2004
Abstract
Software architectures and architectural styles are increasingly used for designing large-scale software systems. Alfa is a framework for the composition of style-based software architectures from a small set of primitives. It models the behavior of architectural components and connectors as orderings among events at their inputs and outputs. Formalizing such behavior is useful for checking conformance of architectures to their styles. We therefore propose a formal approach that uses data-abstract constraint automata to model the behavior of Alfa's compositions, and to verify their behavioral style conformance. We have also developed an automated conformance analyzer for Alfa. © 2004 IEEE
Integrating model checking and deduction for Rebeca
, Article Scientia Iranica ; Volume 12, Issue 1 , 2005 , Pages 55-65 ; 10263098 (ISSN) ; Movaghar, A ; Sharif University of Technology
Sharif University of Technology
2005
Abstract
Rebeca is an actor-based language for modeling concurrent and distributed systems. Its Java-like syntax makes it easy-to-use for practitioners and its formal foundation is a basis to make different formal verification approaches applicable. Compositional verification and abstraction techniques are used in formal verification of Rebeca models to overcome state explosion problems. The main contribution of this paper is to show how model checking and deduction are integrated for verifying certain properties of these models. Deduction is used to prove that abstraction techniques preserve a set of behavioral specifications in temporal logic and is also used in applying the compositional...
Conceptual Evaluation of Brain Internal Models and Modeling their Uncertainty
, M.Sc. Thesis Sharif University of Technology ; Jahed, Mehran (Supervisor)
Abstract
In the literature of motor behavior, rapid and harmonious human movements and adaptation to limb dynamics are described with reference to internal models. Concepts of internal models in neuroscience cognitive sciences and computational modeling have been investigated and their structure and performance have been evaluated by behavioral, neurophysiological and medical imaging data. The purpose of the theory of internal models is to explain the mechanism of human movement. Based on this theory, the central nervous system uses internal models to predict and adjust movements and reduce uncertainty. Uncertainty refers to the unknown dynamics of the system due to the lack of access to accurate...
Vulnerability analysis of networks to detect multiphase attacks using the actor-based language Rebeca
, Article Computers and Electrical Engineering ; Volume 36, Issue 5 , 2010 , Pages 874-885 ; 00457906 (ISSN) ; Makarem, M. S ; Sirjani, M ; Jalili, R ; Movaghar, A ; Sharif University of Technology
2010
Abstract
Increasing use of networks and their complexity make the task of security analysis more and more complicated. Accordingly, automatic verification approaches have received more attention recently. In this paper, we investigate applying of an actor-based language based on reactive objects for analyzing a network environment communicating via Transport Protocol Layer (TCP). The formal foundation of the language and available tools for model checking provide us with formal verification support. Having the model of a typical network including client and server, we show how an attacker may combine simple attacks to construct a complex multiphase attack. We use Rebeca language to model the network...
Model checking in Rebeca
, Article Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, NV, 23 June 2003 through 26 June 2003 ; Volume 4 , 2003 , Pages 1819-1822 ; 1892512416 (ISBN) ; Movaghar, A ; Iravanchi, H ; Jaghoori, M ; Shali, A ; Sharif University of Technology
2003
Abstract
Rebeca is a recently introduced actor-based language, for modeling concurrent and distributed systems. In this paper, we present our work on model checking Rebeca code. Rebeca is a high level language, comparing to the most of languages used for modeling, in the existing model checker tools. So, we need specific abstraction techniques for model checking Rebeca code. Here, we show some of these abstraction techniques used and some case studies
Synthesis of Reo circuits for implementation of component-connector automata specifications
, Article 7th International Conference on Coordination Models and Languages, COORDINATION 2005, Namur, 20 April 2005 through 23 April 2005 ; Volume 3454 , 2005 , Pages 236-251 ; 03029743 (ISSN) ; Baier, C ; De Boer, F ; Rutten, J ; Sirjani, M ; Sharif University of Technology
Springer Verlag
2005
Abstract
Composition of a concurrent system out of components involves coordination of their mutual interactions. In component-based construction, this coordination becomes the responsibility of the glue-code language and its underlying run-time middle-ware. Reo offers an expressive glue-language for construction of coordinating component connectors out of primitive channels. In this paper we consider the problem of synthesizing Reo coordination code from a specification of a behavior as a relation on scheduled-data streams. The specification is given as a constraint automaton that describes the desired input/output behavior at the ports of the components. The main contribution in this paper is an...
Modular verification of a component-based actor language
, Article Journal of Universal Computer Science ; Volume 11, Issue 10 , 2005 , Pages 1695-1717 ; 0958695X (ISSN) ; De Boer, F. S ; Movaghar, A ; Sharif University of Technology
2005
Abstract
Rebeca is an actor-based language for modeling concurrent and distributed systems as a set of reactive objects which communicate via asynchronous message passing. Rebeca is extended to support synchronous communication, and at the same time components are introduced to encapsulate the tightly coupled reactive objects which may communicate by synchronous messages. This provide us a language for modeling globally asynchronous and locally synchronous systems. Components interact only by asynchronous messages. This feature and also the eventdriven nature of the computation are exploited to introduce a modular verification approach in order to overcome the state explosion problem in model...
Runtime Analysis of Self-adaptive Systems
, Ph.D. Dissertation Sharif University of Technology ; Movaghar, Ali (Supervisor) ; Sirjani, Marjan (Supervisor)
Abstract
Increasing the complexity of software systems, their ubiquitous presence in the human activities, and necessity to preserving the functional and nonfunctional requirements of the systems under an uncertain environment, increase the need for self-adaptive systems. A self-adaptive system changes its structure and behaviors in response to changes in its environment and the system itself. A key research challenge in the self-adaptive community is to guarantee that the system fulfills its requirements. This issue can be addressed by employing formal methods during the design of the software systems. However, the assurance techniques should be used during the execution of the system as well as the...
Extended Rebeca: A component-based actor language with synchronous message passing
, Article 5th International Conference on Application of Concurrency to System Design, ACSD 2005, St. Malo, 7 June 2005 through 9 June 2005 ; Volume 2005 , 2005 , Pages 212-220 ; 15504808 (ISSN); 0769523633 (ISBN); 9780769523637 (ISBN) ; De Boer, F ; Movaghar, A ; Shali, A ; Sharif University of Technology
2005
Abstract
In this paper, we propose extended Rebeca as a tool-supported actor-based language for modeling and verifying concurrent and distributed systems. We enrich Rebeca with a formal concept of components which integrates the message-driven computational model of actor-based languages with synchronous message passing. Components are used to encapsulate a set of internal active objects which react asynchronously to messages by means of methods and which additionally interact via a synchronous message passing mechanism. Components themselves interact only via asynchronous and anonymous messages. We present our compositional verification approach and abstraction techniques, and the theory...
Model checking, automated abstraction, and compositional verification of Rebeca models
, Article Journal of Universal Computer Science ; Volume 11, Issue 6 , 2005 , Pages 1054-1082 ; 0958695X (ISSN) ; Movaghar, A ; Shali, A ; De Boer, F. S ; Sharif University of Technology
2005
Abstract
Actor-based modeling, with encapsulated active objects which communicate asynchronously, is generally recognized to be well-suited for representing concurrent and distributed systems. In this paper we discuss the actor-based language Rebeca which is based on a formal operational interpretation of the actor model. Its Java-like syntax and object-based style of modeling makes it easy to use for software engineers, and its independent objects as units of concurrency leads to natural abstraction techniques necessary for model checking. We present a front-end tool for translating Rebeca to the languages of existing model checkers in order to model check Rebeca models. Automated modular...
Modeling and verification of reactive systems using rebeca
, Article Fundamenta Informaticae ; Volume 63, Issue 4 , 2004 , Pages 385-410 ; 01692968 (ISSN) ; Movaghar, A ; Shali, A ; De Boer, F. S ; Sharif University of Technology
2004
Abstract
Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their correctness. In this paper, we develop an actor-based model for describing such systems, use temporal logic to specify properties of the model, and apply different abstraction and verification methods for verifying that the model meets its specification. We use a compositional verification approach for verifying safety properties of these models. For that we introduce a notion of component, based on an user-defined decomposition of the model....
Coordinated actors for reliable self-adaptive systems
, Article Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 19 October 2016 through 21 October 2016 ; Volume 10231 LNCS , 2017 , Pages 241-259 ; 03029743 (ISSN) ; 9783319576657 (ISBN) ; Akkaya, I ; Khamespanah, E ; Khakpour, N ; Sirjani, M ; Movaghar, A ; Lee, E. A ; Khosravi, R ; Kouchnarenko, O ; Sharif University of Technology
2017
Abstract
Self-adaptive systems are systems that automatically adapt in response to environmental and internal changes, such as possible failures and variations in resource availability. Such systems are often realized by a MAPE-K feedback loop, where Monitor, Analyze, Plan and Execute components have access to a runtime model of the system and environment which is kept in the Knowledge component. In order to provide guarantees on the correctness of a self-adaptive system at runtime, the MAPE-K feedback loop needs to be extended with assurance techniques. To address this issue, we propose a coordinated actor-based approach to build a reusable and scalable model@runtime for self-adaptive systems in the...
Probability of missed detection as a criterion for receiver placement in MIMO PCL
, Article IEEE National Radar Conference - Proceedings, 7 May 2012 through 11 May 2012, Atlanta, GA ; 2012 , Pages 0924-0927 ; 10975659 (ISSN) ; 9781467306584 (ISBN) ; Chitgarha, M. M ; Radmard, M ; Nayebi, M. M ; Sharif University of Technology
IEEE
2012
Abstract
Using multiple antennas at the transmit and receive sides of a passive radar brings both the benefits of MIMO radar and passive radar. However one of the obstacles arisen in such configuration is the receive antennas placement in proper positions so that the radar performance is improved. Here we just consider the case of positioning one receiver among multiple illuminators of opportunity. Indeed it is a start for the solution of optimizing the geometry of the multiple receivers in a passive radar
An efficient method for the ring opening of epoxides with aromatic amines by Sb(III) chloride under microwave irradiation
, Article Journal of Chemical Research ; Issue 4 , 2008 , Pages 220-221 ; 03082342 (ISSN) ; Hashemi, M. M ; Mottaghi, M. M ; Foroughi, M. M ; Sharif University of Technology
2008
Abstract
SbCl3 supported on montmorillonite K-10 is an efficient catalyst for the ring opening of epoxides with aromatic amines under solvent-free conditions and microwave irradiation to give the corresponding b-amino alcohols in high yields with high regioselectivity
Resource allocation for uav-enabled integrated sensing and communication (isac) via multi-objective optimization
, Article ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings ; Volume 2023-June , 2023 ; 15206149 (ISSN); 978-172816327-7 (ISBN) ; Naghsh, M. M ; Karbasi, M ; Nayebi, M. M ; Sharif University of Technology
Institute of Electrical and Electronics Engineers Inc
2023
Abstract
In this paper, we consider an integrated sensing and communication (ISAC) system with wireless power transfer (WPT) where an unmanned aerial vehicle (UAV)-based radar serves a group of energy-limited communication users in addition to its sensing functionality. In this architecture, the radar senses the environment in phase 1 (namely sensing phase) and mean-while, the communications users (nodes) harvest and store the energy from the radar transmit signal. The stored energy is then used for information transmission from the nodes to UAV in phase 2, i.e., uplink phase. Performance of the radar system depends on the transmit signal as well as the receive filter; the energy of the transmit...
MIMO radar signal design to improve the MIMO ambiguity function via maximizing its peak
, Article Signal Processing ; Volume 118 , 2016 , Pages 139-152 ; 01651684 (ISSN) ; Radmard, M ; Nazari Majd, M ; Karbasi, S. M ; Nayebi, M. M ; Sharif University of Technology
Elsevier
2016
Abstract
One of the important obstacles in MIMO (Multiple Input Multiple Output) radars is the issue of designing proper transmit signals. Indeed, the capability of signal design is a significant advantage in MIMO radars, through which, the system can achieve much better performance. Many different aspects of this performance improvement have been considered yet, and the transmit signals have been designed to attain such goal, e.g., getting higher SNR or better detector's performance at the receiver. However, an important tool for evaluating the radar's performance is its ambiguity function. In this paper, we consider the problem of transmit signal design, in order to optimize the ambiguity function...