1 - 2 of 2
ItemExpressing early behavior specifications with branching visual scenarios(Edutecne, 2018-11)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.
ItemExploring specification pattern based behavioral synthesis with scenario clauses(Universidad Nacional del Centro de la Provincia de Buenos Aires, 2018-10)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.