AN INTERACTIVE SYSTEM DESIGN METHOD BASED ON A FORMAL SPECIFICATION OF A USER TASK

提出了一种交互系统设计的形式化方法。在该方法中，通过任务流图来构建任务模型。任务流图的语义由LOTOS形式化定义，LOTOS是一种基于进程代数的形式化规范语言。通过将每个任务分解成表示系统动作和用户动作的多个子任务来细化任务流程图。其次，提出了一种任务模型的形式化验证方法。在我们的方法中，通过一个基于模型检测的验证工具CADP对从任务流图中得到的LOTOS规范进行了验证。提出了一种基于抽象时序机(ASM)规格说明的用户界面形式化描述方法，并讨论了基于ASM规格说明的原型生成方法。介绍了一个抽象窗口系统(AWS)，它是一个简单的多进程模型，每个用户界面模块通过发送或接收消息来异步操作。每个UI模块都被建模为AWS的一个组件，并由ASM规范定义。我们实现了一个编译器，将用户界面的ASM规范转换为Java程序。使用该编译器的经验表明，该方法是有效的。

A formal method for interactive system design is proposed. In the proposed method, a task model is constructed by a task flow diagram. The semantics of a task flow diagram is formally defined by LOTOS, which is a formal specification language based on the process algebra. A task flow diagram is refined by decomposing each task into several subtasks which represent system actions and user actions. Next a formal verification method for a task model is proposed. In our method, the LOTOS specification derived from a task flow diagram is verified by a model checking-based verification tool CADP. We also present an automatic prototype generation method which translates a task model into an HTML and a CGI program.A formal description method of user interface (UI) based on a subclass of algebraic specifications called abstract sequential machine (ASM) specifications is proposed and a prototype generation method from an ASM specification is discussed We introduce an abstract window system (AWS), which is a simple multiprocess model where each UI module behaves asynchronously by sending or receiving messages. Each UI module is modeled as a component of the AWS and is defined by an ASM specification. We implemented a compiler which translates an ASM specification of UI into a Java program. Experiences with the compiler showed the effectiveness of the proposed method.