Encontrados 21 documentos, a visualizar página 1 de 3
Giving ALLOY a family
Neves, Renato; Madeira, Alexandre; Martins, Manuel A.; Barbosa, L. S.Lightweight formal methods ought to provide to the end user the rigorousness of mathematics, without compromising simplicity and intuitiveness. ALLOY is a powerful tool, particularly successful on this mission. Limitations on the verification side, however, are known to prevent its wider use in the development of safety or mission critical applications. A number of researchers proposed ways to connect Alloy to ...
Hybridisation at work
Neves, Renato; Madeira, Alexandre; Martins, Manuel A.; Barbosa, L. S.This paper presents the encoding of the hybridisation method into the HETS platform.
Boilerplates for reconfigurable systems : a language and its semantics
Madeira, Alexandre; Martins, Manuel A.; Barbosa, L. S.Boilerplates are simplified, normative English texts,intended to capture software requirements in a controlled way. This paper proposes a pallet of boilerplates as a requirements modelling language for reconfigurable systems, i.e., systems structured in different modes of execution among which they can dynamically commute. The language semantics is given as an hybrid logic, in an institutional setting. The mild...
When even the interface evolves ...
Madeira, Alexandre; Neves, Renato; Martins, Manuel A.; Barbosa, L. S.This paper extends the authors’ previous work on a formal approach to the specification of reconfigurable systems in which configurations are taken as local states in a suitable transition structure. The novelty is the explicit consideration that not only the realisation of a service may change from a configuration to another, but also the set of services provided and even their functionality, may themselves va...
Hybridization of institutions
Martins, Manuel A.; Madeira, A.; Diaconescu, R.; Barbosa, L.S.Modal logics are successfully used as specification logics for reactive systems. However, they are not expressive enough to refer to individual states and reason about the local behaviour of such systems. This limitation is overcome in hybrid logics which introduce special symbols for naming states in models. Actually, hybrid logics have recently regained interest, resulting in a number of new results and techn...
Hybridization of institutions
Martins, Manuel A.; Madeira, A.; Diaconescu, R.; Barbosa, L. S.Extended version including all proofs ; Modal logics are successfully used as specification logics for reactive systems. However, they are not expressive enough to refer to individual states and reason about the local behaviour of such systems. This limitation is overcome in hybrid logics which introduce special symbols for naming states in models. Actually, hybrid logics have recently regained interest, resul...
Refinement by interpretation in Pi-institutions
Rodrigues, César J.; Martins, Manuel A.; Madeira, A.; Barbosa, L. S.The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of π-institutions. This leads to a smooth generalization of the “refinement by interpretation” approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to build up a ref...
Hybrid specification of reactive systems : an institutional approach
Madeira, A.; Faria, José Miguel; Martins, Manuel A.; Barbosa, L. S.This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the correspond...
Models as arrows : the role of dialgebras
Martins, Manuel A.; Madeira, A.; Barbosa, L. S.A large number of computational processes can suitably be described as a combination of construction, i.e. algebraic, and observation, i.e. coalgebraic, structures. This paper suggests dialgebras as a generic model in which such structures can be combined and proposes a small calculus of dialgebras including a wrapping combinator and se- quential composition. To take good care of invariants in software design, ...
Reasoning about complex requirements in a uniform setting
Martins, Manuel A.; Madeira, A.; Barbosa, L. S.The paper formulates HEQ, an institution for hybrid equational logic to provide a uniform setting to express and reasoning about different sorts of properties of complex software. It is also shown how, through the definition of a suitable comorphism to FOL, this can be integrated in Hets, providing suitable tool support for teaching and re- search. The whole exercise was motivated by the need to unify, in a sin...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||