Expressing early behavior specifications with branching visual scenarios

No Thumbnail Available
Asteasuain, Fernando
Gamboa, Pablo Daniel
Calonge, Federico
D’Angiolo, Federico
Díaz, Federico
Journal Title
Journal ISSN
Volume Title
Branching logics enable the software engineer to express interesting type of properties and feature more efficient algorithms for model checking than linear logics. In this work we present an extension of the FVS language (based on a linear representation of systems' execution) in order to contemplate branching properties. The formal semantics of this extension, named Branching FVS, is also introduced in this work. As a case of study we model the behavior of a FLASH memory test chip, a classical hardware verification example. This is a particular domain where branching logics are heavily used to specify the expected behavior of systems.
formal verification, branching behavior, model checking
Asteasuain,F.; Calonge,F.; D’Angiolo, F.; Díaz, F.; Gamboa, P. (2018). Expressing early behavior specifications with branching visual scenarios. En: Roberto Sotomayor, Lucia Rosario Malbernat, Miguel Méndez Garabetti; Felipe Evans (Comps.), CoNaIISI 2018 - Congreso Nacional de Ingeniería Informática – Sistemas de Información, Mar del Plata, Argentina, 2018, pp.1106-1112