A description of some of our past research topics.
In this project, we proposed a new simple formal method, which combines various features such as modularity, code generation and automatic verification, to give a scalable notation to specify, design, validate and verify GUIs. Our approach, called Visual Event Grammars (VEG) is based on decomposing the specification of a large GUI into communicating automata. Breaking a complex scene down into communicating pieces may dramatically diminish the number of states, as shown by popular notations such as Statecharts.