Sharif Digital Repository

In our previous work, we presented a Z-based formalism, called NZ, by which one can explicitly specify bounded, unbounded, erratic, angelic, demonic, loose, strict, singular, and plural nondeterminism. The NZ notation is mainly based on a new notion of operation schemas, called multi-schema. Since the operations of the Z schema calculus do not work on multi-schemas anymore, in this paper we augment NZ with a new set of schema calculus operations that can be applied on multi-schemas as well as ordinary operation schemas. To demonstrate the usability of the resulting formalism, we show how this formalism can assist to model game-like situations and concurrent systems as two well-known classes... 

Constraint automata are formalisms to describe the behavior and possible data flow in coordination models. In this paper we introduce a linear time temporal logic, called temporal logic of steps (TLS), for specifying the executions of constraint automata. TLS is the first attempt in presenting a linear temporal logic for constraint automata. Having TLS in hand, we are able to design model checking algorithms for verification of concurrent systems modeled by constraint automata. © 2008 Springer-Verlag  

In the last two decades, a number of architecture-based software development notations, methods, techniques, and tools were formulated. Of particular interest to the software architecture researchers and practitioners were the notations and languages for modeling software architectures, known as ADLs. Object Stochastic Activity Network (OSAN) is a new model which inherits useful features from Petri nets, stochastic activity networks and queue networks, which made it a powerful and flexible tool to model concurrent systems and evaluate and verify them. This paper introduces OSAN as a new analyzable architecture description language, which can be used both for modeling architectural aspects of... 

Model checking is a formal method for verifying finite state systems properties. μ-calculus is a very expressive fix point logic capable of specifying a wide range of properties of finite state, reactive and concurrent systems. In this paper, we present a new model checking algorithm for linear and a fragment of indexed modal μ - calculus. This algorithm is based on the method of characterization of fixed point temporal logics formulae using automata. We use first recurrence automata for this purpose. Our algorithm is linear time on the size of the system model. The main contributions of this work are the efficiency of the algorithm and the first use of first recurrence automata for μ...