The Role of Visual Tools in a Web Application Design and Verification Framework: A Visual Notation for LTL Formulae

As the Web becomes a platform for implementing complex B2C and B2B applications, there is a need to extend Web conceptual modeling to process-centric applications. In this context, new problems about process safety and verification arise. Recent work has investigated high-level specification and verification of Web applications. This relies on a formal data-driven model of the application, which can access an underlying database as well as state information updated as the interaction progresses, and a set of user inputs. Properties verified concern the sequences of events, inputs, states, and actions resulting from the interaction. For the purpose of automatic verification, properties are expressed in linear-time or branching-time temporal logics. However, temporal logics properties are difficult to specify and understand by users, which can be a significant obstacle to the practical use of verification tools. In the present paper, we propose two alternative visual notations for specif...

• Type: Conference
• Year: 2005
• Where: ICWE
• Authors: Marco Brambilla, Alin Deutsch, Liying Sui, Victor Vianu
• Keywords: Branching-time Temporal Logics, ICWE 2005, Temporal Logics, Temporal Properties