20 documents found, page 1 of 2
Paraconsistent transition systems
Cruz, Ana; Madeira, Alexandre; Barbosa, Luís S.Often in Software Engineering, a modeling formalism has to support scenarios of inconsistency in which several requirements either reinforce or contradict each other. Paraconsistent transition systems are proposed in this paper as one such formalism: states evolve through two accessibility relations capturing weighted evidence of a transition or its absence, respectively. Their weights come from a specific resi...
Software engineering for 'quantum advantage'
Barbosa, Luís S.Software is a critical factor in the reliability of computer systems. While the development of hardware is assisted by mature science and engineering disciplines, software science is still in its infancy. This situation is likely to worsen in the future with quantum computer systems. Actually, if quantum computing is quickly coming of age, with potential groundbreaking impacts on many different fields, such ben...
A logic for the stepwise development of reactive systems
Madeira, Alexandre Leite Castro; Barbosa, Luís S.; Hennicker, Rolf; Martins, Manuel A.D↓is a new dynamic logic combining regular modalities with the binder constructor typical of hybrid logic, which provides a smooth framework for the stepwise development of reactive systems. Actually, the logic is able to capture system properties at different levels of abstraction, from high-level safety and liveness requirements, to constructive specifications representing concrete processes. The paper discus...
A logic for the stepwise development of reactive systems
Madeira, Alexandre; Barbosa, Luís S.; Hennicker, Rolf; Martins, Manuel A.D↓ is a new dynamic logic combining regular modalities with the binder constructor typical of hybrid logic, which provides a smooth framework for the stepwise development of reactive systems. Actually, the logic is able to capture system properties at different levels of abstraction, from high-level safety and liveness requirements, to constructive specifications representing concrete processes. The paper discu...
Reuse and integration of specification logics: the hybridisation perspective
Barbosa, Luís S.; Martins, Manuel A.; Madeira, Alexandre; Neves, RenatoHybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specifi...
A method for rigorous design of reconfigurable systems
Madeira, Alexandre; Neves, Renato; Barbosa, Luís S.; Martins, Manuel A.Reconfigurability, understood as the ability of a system to behave differently in different modes of operation and commute between them along its lifetime, is a cross-cutting concern in modern Software Engineering. This paper introduces a specification method for reconfigurable software based on a global transition structure to capture the system’s reconfiguration space, and a local specification of each operation m...
A dynamic logic for every season
Madeira, Alexandre; Neves, Renato; Martins, Manuel A.; Barbosa, Luís S.This paper introduces a method to build dynamic logics with a graded semantics. The construction is parametrized by a structure to support both the spaces of truth and of the domain of computations. Possible instantiations of the method range from classical (assertional) dynamic logic to less common graded logics suitable to deal with programs whose transitional semantics exhibits fuzzy or weighted behaviour. T...
Completeness and decidability results for hybrid(ised) logics
Neves, Renato; Martins, Manuel A.; Barbosa, Luís S.Adding to the modal description of transition structures the ability to refer to specific states, hybrid(ised) logics provide an interesting framework for the specification of reconfigurable systems. The qualifier ‘hybrid(ised)’ refers to a generic method of developing, on top of whatever specification logic is used to model software configurations, the elements of an hybrid language, including nominals and mod...
Architectural prototyping: from CCS to .Net
F. Rodrigues, Nuno; Barbosa, Luís S.Over the last decade, software architecture emerged as a critical issue in Software Engineering. This encompassed a shift from traditional programming towards software development based on the deployment and assembly of independent components. The specification of both the overall systems structure and the interaction patterns between their components became a major concern for the working developer. Although a...
COORDINSPECTOR: a tool for extracting coordination data from legacy code
F. Rodrigues, Nuno; Barbosa, Luís S.More and more current software systems rely on non trivial coordination logic for combining autonomous services typically running on different platforms and often owned by different organizations. Often, however, coordination data is deeply entangled in the code and, therefore, difficult to isolate and analyse separately. COORDINSPECTOR is a software tool which combines slicing and program analysis techniques t...