Consiglio Nazionale delle Ricerche

Tipo di prodottoArticolo in rivista
TitoloA scalable formal method for design and automatic checking of user interfaces
Anno di pubblicazione2005
Autore/iJean Berstel; Stefano Crespi-Reghizzi; Gilles Roussel; Pierluigi San Pietro
Affiliazioni autoriInstitut Gaspard-Monge, Université de Marne-la-Vallée, France Politecnico di Milano, Milano, Italia
Autori CNR e affiliazioni
  • inglese
AbstractThe article addresses the formal specification, design and implementation of the behavioral com- ponent of graphical user interfaces. The complex sequences of visual events and actions that con- stitute dialogs are specified by means of modular, communicating grammars called VEG (Visual Event Grammars), which extend traditional BNF grammars to make them more convenient to model dialogs. A VEG specification is independent of the actual layout of the GUI, but it can easily be integrated with various layout design toolkits. Moreover, a VEG specification may be verified with the model checker SPIN, in order to test consistency and correctness, to detect deadlocks and unreachable states, and also to generate test cases for validation purposes. Efficient code is automatically generated by the VEG toolkit, based on compiler technology. Realistic applications have been specified, verified and implemented, like a Notepad-style editor, a graph construction library and a large real application to medical software. It is also argued that VEG can be used to specify and test voice interfaces and multimodal dialogs. The major contribution of our work is blending together a set of features coming from GUI design, compilers, software engineering and formal verification. Even though we do not claim novelty in each of the techniques adopted for VEG, they have been united into a toolkit supporting all GUI design phases, that is, specification, design, verification and validation, linking to applications and coding.
Lingua abstractinglese
Altro abstract-
Lingua altro abstract-
Pagine da124
Pagine a167
Pagine totali-
RivistaACM transactions on software engineering and methodology
Attiva dal 1992
Editore: Association for Computing Machinery, - New York, NY
Paese di pubblicazione: Stati Uniti d'America
Lingua: inglese
ISSN: 1049-331X
Titolo chiave: ACM transactions on software engineering and methodology
Titolo proprio: ACM transactions on software engineering and methodology.
Titolo abbreviato: ACM trans. softw. eng. methodol.
Titoli alternativi:
  • Transactions on software engineering and methodology
  • Association for Computing Machinery transactions on software engineering and methodology
Numero volume della rivista14
Fascicolo della rivista2
Verificato da refereeSì: Internazionale
Stato della pubblicazione-
Indicizzazione (in banche dati controllate)
  • ISI Web of Science (WOS) (Codice:000229287800001)
Parole chiaveHuman-computer interaction (HCI), applications of model checking, GUI design
Link (URL, URI)-
Titolo parallelo-
Data di accettazione-
Note/Altre informazioni-
Strutture CNR
  • IEIIT — IEIIT - Sede secondaria di Milano
Moduli CNR
    Progetti Europei-
    • Design and automatic checking

    Dati associati a vecchie tipologie
    I dati associati a vecchie tipologie non sono modificabili, derivano dal cambiamento della tipologia di prodotto e hanno solo valore storico.
    • ACM Press, New York (Stati Uniti d'America)