Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
Ian MacColl , University of Queensland
David Carrington , University of Queensland
In this paper we define a translation from the User Action Notation (UAN) to the process algebra Communicating Sequential Processes (CSP). UAN is an informal notation, used for task modeling and design. Translating a UAN task description to CSP provides a basis for rigorous development of an interactive system. The resulting CSP description is a suitable abstract starting point for development, as it describes externally visible behaviour with no mention of presented or underlying state. Our translation covers all UAN constructs except for waiting, interruptibility and true concurrency, which cannot be expressed in interleaving, untimed CSP. Our approach integrates task models, typically based on user-oriented concerns, into rigorous development, which is typically system-oriented. It provides a basis for a framework for formal development of interactive systems.
I. MacColl and D. Carrington, "Translating UAN into CSP," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 121.