Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 19th Brazilian Symposium on Formal Methods, SBMF 2016, which took place in Natal, Brazil, in November 2016.
The 12 papers presented together with two invited talks were carefully reviewed and selected from 22 submissions. They are organized in the following topical sections: analysis and verification; modeling and logic; and model checking.

Inhaltsverzeichnis

Frontmatter

Invited Talks

Frontmatter

Formal Model-Based Constraint Solving and Document Generation

Constraint solving technology for formal models has made considerable progress in the last years, and has lead to many applications such as animation of high-level specifications, test case generation, or symbolic model checking. In this article we discuss the idea to use formal models themselves to express constraint satisfaction problems and to embed formal models as executable artefacts at runtime. As part of our work, we have developed a document generation feature, whose output is derived from such executable models. This present article has been generated using this feature, and we use the feature to showcase the suitability of formal modelling to express and solve various constraint solving benchmark examples. We conclude with current limitations and open challenges of formal model-based constraint solving.
Michael Leuschel

Formal Testing from Natural Language in an Industrial Context

We present some results on developing formal testing strategies and tools for mobile applications, in the context of a partnership with Motorola, a Lenovo company. Actually, the overall scope is much larger, encompassing image processing, optimisation algorithms, sentiment analysis, energy-aware software design, and other research areas.
Augusto Sampaio, Filipe Arruda

Analysis and Verification

Frontmatter

Application of Formal Methods to Verify Business Processes

Formal specifications and modeling languages can be used to provide support for Business Process (BP) analysts and designers to verify the behavior of BPs with respect to business performance indicators (i.e., service time, waiting time or queue size). This article presents the application of the Timed Automata (TA) formal language to check BPs modeled with Business Process Model and Notation (BPMN) using the model checking verification technique. Also, a set of transformation rules and two algorithms are introduced to obtain TA-networks from BPMN models, allowing the formal specification of a BP-task model equivalent to the BPMN model. The approach presented here contributes to conduct the qualitative analysis of BPMN models.
Luis E. Mendoza Morales, Carlos Monsalve, Mónica Villavicencio

An Approach for Verifying Educational Robots

Virtual robot programming environments provide a visual interface for programming and simulating educational robots. Nowadays, simulation is the only way to assess the robot behaviour inside such environments, as there is no approach that supports the automatic analysis of the correctness of robot programs. This paper introduces an automatic approach for verifying robot programs written in the educational programming language ROBO. We give semantics for ROBO programs in the setting of CSP process algebra and automatically verify the properties of the programs using the FDR refinement checker. The verification approach has been defined considering programming exercises proposed in the literature on educational robotics. We illustrate the approach using sample programs written in ROBO and discuss how to integrate such an approach with educational tools.
Sidney Nogueira, Taciana Pontual Falcão, Alexandre Mota, Emanuel Oliveira, Itamar Moraes, Iverson Pereira

Verigraph: A System for Specification and Analysis of Graph Grammars

Graph grammars are models that allow for a visual representation of both static and dynamic aspects of a system. There are several tools that allow the edition, simulation and analysis of graph grammars, each of them focusing on one kind of analysis technique or graph model. In this paper we present a new tool for simulation and analysis of graph grammars, called Verigraph, built with the following design principles: an implementation as direct as possible of formal concepts (to ease correctness arguments), a generic implementation of core algorithms (to allow its application for several graph models), and a reasonable running time. In this paper we present architectural aspects of Verigraph, together with a comparison with other similar tools in terms of available features.
Andrei Costa, Jonas Bezerra, Guilherme Azzi, Leonardo Rodrigues, Thiago Rafael Becker, Ricardo Gabriel Herdt, Rodrigo Machado

Modeling and Logic

Frontmatter

Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition

Efficient reuse is a goal of many software engineering strategies and is useful in the safety-critical domain where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by a component-based reuse strategy. In previous work, we outlined a component-based reuse methodology for Event-B. The methodology provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We developed a process for creating library components, composing them, and for specifying new properties (involving the composed elements). We introduced Event-B component interfaces and propose to use a diagrammatic representation of component instances. However, in that approach, the communication between components is modelled in an abstract manner. In this paper, we describe a more concrete specification approach which includes interfaces with ‘callable’ interface events. These events model operations, and additional syntactic constructs model their invocation.
Andrew Edmunds, Marina Waldén

Algebraic Foundations for Specification Refinements

In this paper we present a mathematical framework tailored for reasoning about specification/program refinements. The proposed framework uses formal concepts coming from Institution Theory and Category Theory, such as theories and morphisms, to capture the notion of specification/program refinement. The main benefits of the proposed mathematical theory are its generality and compositionality, that is, it is based on abstract concepts that can be used to reason about refinements in different formal settings (such as Z, B, VDM, Alloy, statecharts and others), as well as it heavily relies upon the notion of component, thus enabling modular reasoning over the process of specification/program refinement.
Pablo F. Castro, Nazareno Aguirre

On Interval Dynamic Logic

The wide number of languages and programming paradigms, as well as the heterogeneity of ‘programs’ and ‘executions’ require new generalisations of propositional dynamic logic. The dynamisation method, introduced in [20], contributed on this direction with a systematic parametric way to construct Many-valued Dynamic Logics able to handle systems where the uncertainty is a prime concern. The instantiation of this method with the Łukasiewicz arithmetic lattice over [0, 1], that we derive here, supports a general setting to design and to (fuzzy-) reason about systems with uncertainty degrees in their transitions.
For the verification of real systems, however, there are no de facto methods to accommodate exact truth degrees or weights. Instead, the traditional approach within scientific community is to use different kinds of approximation techniques.
Following this line, the current paper presents a framework where the representation values are given by means of intervals. Technically this is achieved by considering an ‘interval version’ of the Kleene algebra based on the [0, 1] Łukasiewicz lattice. We also discuss the ‘intervalisation’ of \(\L \) action lattice (in the lines reported in [28]) and how this class of algebras behaves as an (interval) semantics of many-valued dynamic logic.
Regivan H. N. Santiago, Benjamín Bedregal, Alexandre Madeira, Manuel A. Martins

An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications

Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generation tools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to be written in a particular style, or follow certain patterns, in order to obtain an acceptable performance from the corresponding analyses. Thus, having a formal specification sometimes is not enough for using a particular technique, since such specification may not be provided in the right formalism. In this paper, we deal with this problem in the increasingly common case of having an operational specification, while for analysis reasons requiring a declarative specification. We propose an evolutionary approach to translate an operational specification written in a sequential programming language, into a declarative specification, in relational logic. We perform experiments on a benchmark of data structure implementations, that show that translating representation invariants using our approach and verifying invariant preservation using the resulting specifications outperforms verification with specifications obtained using an existing semantics-preserving translation. Also, our evolutionary computation translation achieves very good precision in this context.
Facundo Molina, César Cornejo, Renzo Degiovanni, Germán Regis, Pablo F. Castro, Nazareno Aguirre, Marcelo F. Frias

A Refinement Repair Algorithm Based on Refinement Game for KMTS Models

In a perspective of an incremental and iterative formal development of software, models should preserve a refinement relation with already existing specifications models. In cases where a model is not a refinement of a specification model, it should be modified in order to create a refinement relation between them. This paper proposes a refinement repair algorithm guided through an analysis of the refinement game between a specification model and another model that is not related by a refinement relation. We are interested in models expressed as Kripke Modal Transitions Systems (KMTS) which are appropriate to represent partial information of systems.
Efraim Machado, Aline Andrade

Massive Open Online Courses and Monoids

Massive open online courses (MOOC) allows for distributed long-distance learning for extremely large student enrollment. Nowadays most universities throughout the world have their courses online. Web portals such as Coursera or edX join together courses from many of them. Even though there are many platforms to support the development of MOOC, such as Moodle or XBlock, it does not seem to be the case that there are many languages to help course descriptions. Moreover, we would like to allow the description of different paths to teach and learn a given subject. We propose Learn, a declarative language for course descriptions. The contribution of this paper is manyfold: (i) we exemplify Learn descriptions, (ii) formalize the meaning of Learn descriptions and teaching strategies, that allows for different teaching paths, and (iii) discuss the implementation of a toolkit to specify, analyze and generate a course in a MOOC platform from Learn descriptions.
Hugo Farias, Christiano Braga, Paulo B. Menezes

Model Checking

Frontmatter

A Bounded Model Checker for Three-Valued Abstractions of Concurrent Software Systems

We present a technique for verifying concurrent software systems via SAT-based bounded model checking. It is based on a direct transfer of the system and an LTL property into a formula that encodes the corresponding model checking problem. In our approach we first employ three-valued abstraction. The state space of the resulting abstract system is then logically encoded, which saves us the expensive construction of an explicit state space model. The verification result can be obtained via two SAT checks. Our work includes the definition of the encoding and a theorem which states that the SAT result for an encoded verification task is equivalent to the result of the corresponding model checking problem. We also introduce an extension of the encoding by fairness constraints, which facilitates the verification of liveness properties. We have implemented our technique in an automatic verification tool that supports bounded LTL model checking under fairness.
Nils Timm, Stefan Gruner, Matthias Harvey

Model Checking Requirements

In software engineering, system requirements are written in a natural language such as English. Later in the design phase, these requirements are usually translated to a semi-formal language such as UML. This design model gives support to the development of the system in a programming language. Although natural language is easy to use, it is intrinsically ambiguous. Undesired effects may arise, as the errors generated by misinterpretation of the requirements can lead to a late discovery of a problem with a costly solution. In this paper, we propose the use of a Controlled Natural Language (CNL) (a subset of English that obeys a formal grammar) as a language for writing requirements. Moreover, we developed a translator from a CNL to the modelling language of the NuSMV model checker. In addition, we propose another CNL to describe properties in the style of a temporal logic. A second translator transforms this CNL into Computation Tree Logic. Therefore, our toolset allows the user to benefit from the user-friendliness of a natural language and to perform a formal analysis on the requirements using the NuSMV model checker. We are thus able to assert whether the requirements satisfy a property. The user only deals with CNLs as we hide all formal languages involved in the inputs of a model checker. Counter-examples are produced in the NuSMV notation, but they are fairly intuitive to understand. We illustrate our work in a case study.
Sérgio Barza, Gustavo Carvalho, Juliano Iyoda, Augusto Sampaio, Alexandre Mota, Flávia Barros

Refinement Verification of Sequence Diagrams Using CSP

During the design of systems, models usually evolve from a conceptual level to a more concrete level that is close to how the implementation should be. In a stepwise development, it is required that lower-level models conform to the properties of higher-level models. In this work, we propose a strategy for verifying the refinement of UML sequence diagrams that uses a formal semantics defined in terms of CSP. In order to allow designers to benefit from this strategy we have implemented it in a modelling tool. Such a tool analyses if a sequence diagram is refined by another, that is, we check if the latter preserves the traces of the former sequence diagram. The main contributions of this paper are: (i) the definition of four different notions of sequence diagrams refinement; (ii) an approach to verify the refinement of sequence diagrams in CSP; and (iii) the development of a tool that allows our refinement notions to be verified without any knowledge of the underlying formal semantics. We illustrate our analysis with a text messaging case study.
Lucas Lima, Juliano Iyoda, Augusto Sampaio

Backmatter

Weitere Informationen

Premium Partner

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung

Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier  - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis.
Jetzt gratis downloaden!

Bildnachweise