A scalable formal method for design and automatic checking of user interfaces (Articolo in rivista)

Type
Label
  • A scalable formal method for design and automatic checking of user interfaces (Articolo in rivista) (literal)
Anno
  • 2005-01-01T00:00:00+01:00 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi
  • 10.1145/1061254.1061256 (literal)
Alternative label
  • Jean Berstel; Stefano Crespi-Reghizzi; Gilles Roussel; Pierluigi San Pietro (2005)
    A scalable formal method for design and automatic checking of user interfaces
    in ACM transactions on software engineering and methodology; ACM Press, New York (Stati Uniti d'America)
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Jean Berstel; Stefano Crespi-Reghizzi; Gilles Roussel; Pierluigi San Pietro (literal)
Pagina inizio
  • 124 (literal)
Pagina fine
  • 167 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume
  • 14 (literal)
Rivista
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroFascicolo
  • 2 (literal)
Note
  • ISI Web of Science (WOS) (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • Institut Gaspard-Monge, Université de Marne-la-Vallée, France Politecnico di Milano, Milano, Italia (literal)
Titolo
  • A scalable formal method for design and automatic checking of user interfaces (literal)
Abstract
  • The 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. (literal)
Editore
Prodotto di
Autore CNR
Insieme di parole chiave

Incoming links:


Prodotto
Autore CNR di
Editore di
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi
Insieme di parole chiave di
data.CNR.it