HASLab

Permanent URI for this community

http://localhost:4000/handle/123456789/30
This service produces reliable software systems in contexts where correctness, responsiveness, robustness and security are essential. It develops integrated research in three lines: formal methods for software development, reliable distributed systems and information security.

Browse

Browsing HASLab by Author "5601"
  • Item
    Computer Aided Verification of Relational Models by Strategic Rewriting
    ( 2017) Visser,J ; Uzal,R ; Necco,CM ; José Nuno Oliveira ; 5601
    Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by point-free binary relational expressions, proof obligations can be expressed as inclusions between relational expressions. We developed a type-directed, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.
  • Item
    Formal Methods – The Next 30 Years
    ( 2019) José Nuno Oliveira ; McIver,A ; ter Beek,MH ; 5601
  • Item
    Formal Methods. FM 2019 International Workshops
    ( 2020) Farrell,M ; Delmas,D ; Monteiro,P ; Kutrib,M ; Dongol,B ; Couto,L ; Cerone,A ; Gonnord,L ; Astarte,T ; Campos,J ; Marmsoler,D ; Luckcuck,M ; Sekerinski,E ; Moreira,N ; José Nuno Oliveira ; Ratiu,D ; Guidotti,R ; 5601
  • Item
    Formal Methods. FM 2019 International Workshops
    ( 2020) Campos,J ; Astarte,T ; Delmas,D ; Monteiro,P ; Kutrib,M ; Dongol,B ; Couto,L ; Cerone,A ; Gonnord,L ; Sekerinski,E ; Moreira,N ; José Nuno Oliveira ; Ratiu,D ; Guidotti,R ; Farrell,M ; Luckcuck,M ; Marmsoler,D ; 5601
  • Item
    Programming from metaphorisms
    ( 2018) José Nuno Oliveira ; 5601
    This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.
  • Item
  • Item
    Verification of railway network models with EVEREST
    ( 2022) Nuno Moreira Macedo ; Alcino Cunha ; José Creissac Campos ; José Nuno Oliveira ; Rafael Braga Costa ; 5625 ; 5612 ; 5599 ; 5601 ; 8206
    Models-at different levels of abstraction and pertaining to different engineering views-are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model-the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD)-in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions. © 2022 ACM.