Framework para el Desarrollo de Software mediante Modularización Avanzada

Permanent URI for this collection

https://repositorio.uai.edu.ar/handle/123456789/1866

Browse

Recent Submissions

Now showing 1 - 2 of 2
  • Item
    Expressing early behavior specifications with branching visual scenarios
    (Edutecne, 2018-11) Asteasuain, Fernando ; Gamboa, Pablo Daniel ; Calonge, Federico ; D’Angiolo, Federico ; Díaz, Federico
    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.
  • Item
    Exploring specification pattern based behavioral synthesis with scenario clauses
    (Universidad Nacional del Centro de la Provincia de Buenos Aires, 2018-10) Asteasuain, Fernando ; Calonge, Federico ; Dubinsky, Manuel
    The Software Engineering community has identified behavioral specification as one of the main challenges to be addressed for the transference of formal verification techniques such as model checking. In particular, expressivity of the specification language is a key factor, especially when dealing with open systems and controllability of events. In this work we present an extension of the FVS language to denote behavior in open systems. By relying on an existing behavioral synthesis technique based on the specification patterns we show how FVS specification can be used as input to automatically build a controller from its specification.