The main contribution of the current paper is to assess the above formalism by using it to model and simulate Mobile IP, an Internet standard which caters for mobile nodes using IP version 4 addresses. These addresses indicate a fixed point of connection to the internet and the protocol caters for nodes being away from home. By defining the model as a Mobile Petri Net, the graphical notation helps to convey the flow of information, and the executable nature of the model opens the way to simulation, state space exploration and model checking.

In this paper an approach for describing the syntax and semantics of UML Statecharts is presented. It is an example of a generic approach to integrating a visual language in a heterogeneous modelling and simulation environment. A system represented in a visual language is syntactically defined as an attributed graph, with well-formedness rules specified by a set of first-order predicates over the abstract syntax of the graph. The language semantics are specified by an {\em Abstract State Machine} (ASM) parameterized with syntactically-correct attributed graphs. In this paper the key issues in the definition of UML statechart syntax and semantics are highlighted.

This paper reviews a proposal for the modular analysis of Petri nets and its applicability to factory automation systems. It presents new algorithms to harness this modular analysis in the determination of reachable states with specified partial markings, to determine possible deadlocks, both global and local, and also liveness. These algorithms have been implemented in a prototype tool which has then been used to solve a problem in factory automation which, even for relatively simple configurations, can lead to state spaces beyond the capabilities of many analysis tools.

In this article, we present a practical analysis approach that makes use of the modular nature of component-based designs to alleviate the state space explosion problem, a well-known obstacle to system verification. The key is to specify interaction protocols for components using a lightweight formal language and then to utilise these protocols as contracts for independent analysis of the components and their interactions. These protocols are often missing or informally documented. It is demonstrated how consistency properties of closed and open component-based designs can be verified using this divide-and-conquer approach.

Verification of the Futurebus+ Cache Coherence protocol: A case study in model checking
Kylie Williams and Robert Esser
27th Australasian Computer Science Conference (ACSC2004)
18-22 January 2004, Dunedin, New Zealand
Available in PDF (529k)

This paper presents a case study for automatic verification using the Communicating Sequential Processes formalism. The case study concerns the Futurebus+ cache coherency standard; we develop a formal model of the protocol and perform some verification tasks upon it. In the process of doing so, we extend the previous solution by developing a formal specification of cache coherence that is suitable for the verification of both directory and snooping based cache coherence protocols.

Towards a Semantic Basis for Rosetta
Catherine Menon, Charles Lakos, Cindy Kong
27th Australasian Computer Science Conference (ACSC2004)
18-22 January 2004, Dunedin, New Zealand

Rosetta is a specification language for designing hardware and software systems with a view to being able to consider multiple system perspectives concurrently (such as functional correctioness, performance constraints, and physical constraints). It also provides the capability to integrate components from heterogeneous domains, such as software and reconfigurable systems and digital and analog hardware.

This paper explores a semantic framework for Rosetta in terms of category theory. We outline how a specification can be equated with a theory, and the different components which satisfy a specification can be equated with the algebras which satisfy this theory. From this, we define a category consisting of all legal specifications in a given language, and then show how the notions of extension and interaction of specifications can be modelled by means of colimits within this category. This requires a consideration of the different notions of equivalence of specifications, including behavioural equivalence, axiom abstraction and signature abstraction. Finally, we briefly outline how information hiding might be included in the construction of objects within the category of theories.

While the motivation for this work is the semantics of Rosetta, the approach adopted can be applied to other specification languages which support multi-faceted, heterogenous specifications.

Rosetta is a systems level design language that allows algebraic specification of systems through facets. The usual approach to formally describe a specification is to define an algebra that satisfies the specification. Although it is possible to formally describe Rosetta facets with the use of algebras, we choose to use the dual of algebra, i.e. coalgebra, to do so. Coalgebras are particularly suited for describing state-based systems. This makes formally defining state-based Rosetta quite straightforward. For non-state-based Rosetta, the formalization is not as direct, but can still be done with coalgebras by focusing on the behaviors of systems specified. We use denotational semantics to map Rosetta syntactic constructs into a language understood by the coalgebras.

In this paper, we introduce a component-based design methodology and present a practical analysis approach that makes use of the modular nature of component-based designs to alleviate the state space explosion problem, a well-known obstacle to system verification. In addition, the approach is illustrated by application to a non-trivial case study: the production cell. It is shown that not only the basic consistency property, viz. the freedom from unexpected reception and deadlock, but also other important safety properties in the design can be proved.

Process networks are popular for modelling distributed computing and signal processing applications, and multi-processor architectures. At the architecture description level, they have the flexibility to model actual processes using various formalisms. This is especially important where the systems are composed of parts with different characteristics, e.g. control-based or dataflow-oriented. However, this heterogeneity of processes presents a challenge for the analysis of process networks. This research proposes a lightweight method for analysing properties of such networks, such as freedom from unexpected reception and deadlock. The method employs interface automata as a bridge between the architectural model and heterogeneous processes. Thus, the properties are determined by a series of small tasks at both the architecture level and the process level. This separation of concerns simplifies the handling of heterogeneous processes and alleviates the potential state space explosion problem when analysing large systems.

Higher-order Petri nets are a class of high-level Petri nets, in which Petri nets themselves are first-class objects. Here tokens may represent Petri nets and Petri nets may be the values of parameters and variables, as well as the result of computations performed during the occurrence of transitions. These features facilitate a number of very powerful higher-order modelling techniques, making Petri nets much more flexible, compositional, and the resulting models more reusable. This work explores the usefulness of some of these techniques by looking at them from an application point of view and by illustrating them with small to medium-sized application examples.

An important part of the design of complex systems is the evaluation of the large number of potential alternative designs. Due to the number and complexity of design parameters, this design space is potentially huge and very complex. Automating part of the design exploration task can be an invaluable help in finding the optimal or near optimal settings of design parameters. The choice of the most appropriate exploration strategy depends on the nature of the parameters, such as their role in the model, the dimensionality and structure of the design space including the number and location of local optima, etc. This paper advocates the use of higher-order modeling techniques to express exploration strategies. This allows users to formulate them in the same set of languages used to model the original system. Hence the set of design space exploration tools can be extended and parameterized as easily as the model itself. In this paper a higher-order modeling langage is presented. As an example a number of simple exploration tools are modeled and applied to a small optimization problem.

A software development methodology is defined that integrates software specification and validation efforts. The integration helps in achieving the twin goals of correct software with well-defined specifications that document it. The major focus of the paper is on dynamic life-cycle models. We indicate how language analysis of the problem description can be extended to derive not only a static class model for the system but also an initial dynamic life-cycle model. Consistency and completeness checks are provided that further drive the requirements elicitation. A case study is presented that clearly demonstrates the methodology.

Describing the Syntax and Semantics of UML Statecharts in a Heterogeneous Modelling Environment
Yan Jin, Robert Esser and Jörn W. Janneck
Diagrams 2002 - Second International Conference on Theory and Application of Diagrams
Callaway Gardens, Georgia, USA
April 18-20, 2002
Available in pdf (524k)
In Lecture Notes in Artifical Intelligence, Vol. 2317, PP 320-334, Springer

In this paper UML statechart diagrams are used as an example of a generic approach to integrating a visual language in a heterogeneous modelling and simulation environment. A system represented in a visual language is syntactically defined as an attributed graph, with well-formedness rules specified by a set of first-order predicates over the abstract syntax of the graph. The language semantics are specified by an {\em Abstract State Machine} (ASM) parameterized with syntactically-correct attributed graphs. In this paper the key issues in the definition of UML statechart semantics are highlighted.

A Framework for Defining Domain-Specific Visual Languages
Robert Esser and Jörn W. Janneck
Workshop on Domain Specific Visual Languages,
ACM Conference on Object-Oriented Programming, Systems ,languages and Applications OOPSLA-2001
Tampa Bay, Florida, USA
October 14, 2001
http://www.isis.vanderbilt.edu/oopsla2k1
Available in pdf (424k)

For many problem domains domain-specific language} (DSLs) offer users more appropriate notations and abstractions in which to model systems when compared with general purpose programming languages. These benefits can often be amplified if a visual notation is used instead of textual notations. In many problem domains visual notations are preferred by practitioners as they often are the most intuitive representation of a problem. However, the lack of supporting infrastructure for constructing, implementing, and maintaining visual languages in general and domain-specific visual languages (DSVLs) in particular has been an impediment to gaining wider acceptance. This paper describes techniques used in the Moses tool-suite for defining the syntax and semantics of DSVLs, which are very general, yet are built on a few very simple concepts and are therefore easy to apply.

Moses - A Tool Suite for Visual Modelling of Discrete-Event Systems
Robert Esser and Jörn W. Janneck
Symposium on Visual/Multimedia Approaches to Programming and Software Engineering, HCC01
Stresa, Italy
September 5-7, 2001
Available in pdf (600k)

This paper gives an overview of the Moses tool suite, a set of tools for visual language programming. In Moses, visual language syntax is defined by first-order predicates over the abstract syntax of a picture, represented by an attributed graph. One way of specifying language semantics in Moses is by writing an Abstract State Machine that interprets a given attributed graph. This paper shows how the editor is parameterized with a description of a visual language, and discusses briefly the generic architecture used to animate and debug visual programs.

A Predicate-Based Approach to Defining Visual Language Syntax
Jörn W. Janneck and Robert Esser
Symposium on Visual Languages and Formal Methods, HCC01
Stresa, Italy
September 5-7, 2001
Available in pdf (413k)

This paper presents an approach to the specification of visual language syntax. Based on attributed graphs as the notion of abstract syntax, syntactical correctness is specified by a set of predicates over that structure. The proposed technique facilitates the natural embedding of other visual and textual notations, the definition of complex syntactic and static-semantic properties, as well as precise error diagnosis and localization. An editing environment supporting this technique is briefly discussed.

Polymorphic CSP Type Checking
Ping Gao and Robert Esser
Twenty-Fourth Australasian Computer Science Conference (ACSC2001)
Bond University, Gold Coast, Queensland
29th January - 2nd February, 2001
Available in gzipped postscript (36k)

Communicating Sequential Processes (CSP) is a language used to describe and reason about concurrent systems. It consists of a process algebra combined with a functional language. This combination poses unique problems when attempting to design a type checker. In this paper the differences between a conventional functional language type checker and a type checker for the CSP language are discussed. This type checker was developed to identify polymorphic types, an important first step towards the goal of automating data independence. The result of this work has been incorporated into the Adelaide Refinement Checker (ARC) - a CSP based tool suite for model checking concurrent systems.

Exploratory performance evaluation using dynamic and parametric Petri nets
Robert Esser and Jörn W. Janneck
Proceedings of the HPC 2000
Pages 357-364. Society for Computer Simulation, April 2000

An approach, called exploratory simulation, is presented that facilitates the automatic exploration through the configuration and design alternatives of a system. The approach builds upon a few extensions to an otherwise conventional high-level Petri net formalism. As an example, a generic and fully parametric simulation environment is created with this modeling language and subsequently used to automatically evaluate the performance of a simple system.

Communication and Synchronization using Bounded Channels in SUAVE
Peter J. Ashenden, Robert Esser and Philip A. Wilsey
Proceedings of the 1999 International
Hardware Description Languages Conference and Exhibit (HDLCON '99) 
(honourable mention paper).
Made available with permission from Accellera Organization Inc pdf (60k)

This paper described improvements to the abstract interprocess communication features added to VHDL as part of the SUAVE language design. Channel type declarations are extended to allow specification of bounded message buffers. This allows the designer to choose between asynchronous or synchronous message passing semantics. The latter makes models more amenable to formal verification based on state-space exploration. The language is also extended to allow specification of timeout intervals in select statements. This change makes the language more widely applicable, including for description of telecommunication protocols.