Alexander Faithfull, Gian Perrone, and Thomas
IT University of Copenhagen, Denmark
Big Red requires version 3.7 or later of the Eclipse Modeling Tools package, which is available from http://www.eclipse.org/downloads.
Once you have a suitable version of Eclipse:—
Bigraphs have been successful in capturing the syntax and semantics of a number of well-known formalisms (e.g., π-calculus, Petri Nets, CCS, and many more), as well as more diverse applications such as business processes, systems biology, wireless networks, and applications for context-aware systems.
(Each figure is annotated with
black-on-gray monospaced text
giving a corresponding representation in the term
language of the BigMC tool.)
The MoveRoom rule matches a User (represented by a U node), and selects any two rooms that are connected by some name a. It then permits the user to move to the other room, leaving the contents of each room otherwise unchanged.
FinishJob captures the idea of a printer finishing a job (by executing the actual print process), and the job is therefore removed completely from the system by this rule, disconnecting it from its associated user.
JobToPrinter transfers a job from the spool to a printer (represented by a P node) that is co-located with the user associated with that job. (Notice that printers may only contain one job at a time.)
JobToSpool allows a print job (represented by a J node) to be transferred from a user (represented by a U node) to a spool (represented by an S node), adding an identifying link to connect users to their submitted print jobs.
This agent represents a simple office environment:—
Pnode) is connected to the spool (represented by a
Unode) has a print job (represented by a
Jnode), which can be submitted to the spool; and
After both of these rules have fired once — that is, after the job has been submitted to the spool and the user has moved into the printer room — the job can be submitted to the room's printer and then printed.
This more complex environment contains:—
Michaelouter name), who can — as before — submit his job to the spool and move between rooms;
Davidouter name), who can only move fruitlessly between rooms; and
|||O.H. Jensen. Mobile processes in bigraphs. Available at http://www.cl.cam.ac.uk/~rm135/Jensen-monograph.pdf, October 2006. [ bib ]|
|||J. Leifer and R. Milner. Transition systems, link graphs and Petri nets. Journal of Mathematical Structures in Computer Science, 16(6):989-1047, 2006. [ bib | DOI ]|
|||R. Milner. Pure bigraphs: Structure and dynamics. Information and Computation, 204(1):60-122, January 2006. [ bib | DOI ]|
|||T.T. Hildebrandt, H. Niss, and M. Olsen. Formalising Business Process Execution with Bigraphs and Reactive XML. In COORDINATION'06, volume 4038 of Lecture Notes in Computer Science, pages 113-129. Springer-Verlag, January 2006. [ bib | DOI | .pdf ]|
|||T.C. Damgaard and J. Krivine. A generic language for biological systems based on bigraphs. Technical report, Citeseer, 2008. [ bib ]|
|||M. Calder and M. Sevegnani. Process algebra for event-driven runtime verification: a case study of wireless network management. In Integrated Formal Methods, pages 21-23. Springer, 2012. [ bib ]|
|||L. Birkedal, S. Debois, E. Elsborg, T.T. Hildebrandt, and H. Niss. Bigraphical models of context-aware systems. In Foundations of Software Science and Computation Structures, pages 187-201. Springer, 2006. [ bib | DOI ]|