Project/scholarship details
- Project/scholarship ID
108302
- Reference
PTDC/EIA-CCO/108302/2008
- FundRef URI
- Funder
FCT - Fundação para a Ciência e a Tecnologia, I.P.
- Funder's country
Portugal
- Funding program
5876-PPCDTI
- Funding amount
87,172.00 €
- Start date
2010-03-15
- End date
2013-05-30
Documents
An integrated formal methods tool-chain and its application to verifying a file...
Ferreira, Miguel A.; Oliveira, José Nuno FonsecaTool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel (R) Flash File System Core. ...
Refinement by interpretation in a general setting
Martins, Manuel A.; Madeira, A.; Barbosa, L. S.Refinement by interpretation replaces signature morphisms by logic interpretations as a means to translate specifications and witness refinements. The approach was recently introduced by the authors [13] in the context of equational specifications, in order to capture a number of relevant transformations in software design, reuse and adaptation. This paper goes a step forward and discusses the generalization of...
Matrices as arrows! A biproduct approach to typed linear algebra
Oliveira, José Nuno Fonseca; Macedo, Hugo DanielMotivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The deriv...
Programming from Galois connections
Mu, Shin-Cheng; Oliveira, José Nuno FonsecaProblem statements often resort to superlatives such as in eg. “. . . the smallest such number”, “. . . the best approximation”, “. . . the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part). This paper introduces a binary relational combinator which mirrors this linguistic ...
On requirements engineering for reactive systems: a formal methodology
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 and consequently evolve through different operational modes, providing, in each of them, different functionalities. The proposed methodology proceeds in three stages, enriching a simple state- machine with local algebraic specifications. It resorts to an expressive variant of hybrid logic which...
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, ...
Refinement by interpretation in φ-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...
Prototyping a calculus of QoS : aware software components
Martins, André BatistaDissertação de mestrado em Engenharia de Informática; Over the last decade component-based software development arose as a promising paradigm to deal with the ever increasing complexity in software design, evolution and reuse. Such components typically encapsulate a number of services through a public interface which provides limited access to a private state space, paying tribute to the nowadays widespread obj...
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...
Matrices as arrows: why categories of matrices matter
Macedo, Hugo DanielTese de doutoramento em Informática; Due to an expanding dematerialization process, computing devices are pervasive and play vital roles in our everyday. Furthermore, society’s dependence on this technology is spiraling, which turns the dependable word the most important adjective among the computer science community that is responsible for the development and programming of such devices’ behavior. From the sid...
Report
Embed
<script type="text/javascript">
<!--
document.write('<div id="rcaap-widget"></div>');
document.write('<script type="text/javascript" src="https://www.rcaap.pt/snippet?resource=documents&project=FCT%2F5876-PPCDTI%2F108302&fields=id,titles,creators,issueDate,link,descriptions"></script>');
-->
</script>