Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2012 | Buch

The Versatile Synchronous Observer Kapitel lesen Erstes Kapitel lesen

Formal Methods: Foundations and Applications

15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings

herausgegeben von: Rohit Gheyi, David Naumann

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 15th Brazilian Symposium on Formal Methods, SBMF 2012, held in Natal, Brazil, in September 2012; co-located with CBSoft 2012, the Third Brazilian Conference on Software: Theory and Practice. The 14 revised full papers presented together with 2 keynotes were carefully reviewed and selected from 29 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains.

Inhaltsverzeichnis

Frontmatter
The Versatile Synchronous Observer
Abstract
A synchronous observer is an adjunct to a system model that monitors its state variables and raises a signal when some condition is satisfied. Synchronous observers provide an alternative to temporal logic as a means to specify safety properties but have the benefit that they are expressed in the same notation as the system model. Model checkers that do use temporal logic can nonetheless employ synchronous observers by checking for properties such as “never (signal raised).”
The use of synchronous observers to specify properties is well-known; rather less well-known is that they can be used to specify assumptions and axioms, to constrain models, and to specify test cases. The idea underlying all these applications is that the basic model generates more behaviors than are desired, the synchronous observer recognizes those that are interesting, and the model checker is constrained to just the interesting cases. The value in this approach is that it is usually much easier to write recognizers than generators. The approach is best exploited in languages such as SAL that provide explicit first class operators for synchronous and asynchronous composition.
The paper describes and illustrates these applications of synchronous observers.
John Rushby
Thirteen Years of Automated Code Analysis at Microsoft
Abstract
Modern program analysis and model-based tools are increasingly complex and multi-faceted software systems. They analyze models and programs using advanced type systems, model checking or model finding, abstract interpretation, symbolic verification or a combination thereof. In this talk I will discuss and compare 10 program analysis tools, which MSR build during the last 10 years. They include theorem provers, program verifiers, bug finders, malware scanners, and test case generators. I will describe the need for their development, their innovation, and application. These tools had both had considerable impact on the research community, as well as being shipped in Microsoft products such as the Static Driver Verifier or as part of Visual Studio and other, widely-used internal software development tools. I highlight that many of these analyzers build on generic infrastructure, most of which is available outside of Microsoft as well. With every analyzer build there is a new opportunity, and with every solution there is a new challenge problem. Thus, I will conclude with 10 challenges in program analysis which hopefully triggers new aspiring directions in our joint quest of delivering predictable software that is free from defect and vulnerabilities.
Wolfram Schulte
Model Checking Propositional Deontic Temporal Logic via a μ-Calculus Characterization
Abstract
In this paper, we present a characterization of a propositional deontic temporal logic into μ-calculus. This logic has been proposed to specify and reason about fault tolerant systems, and even though is known to be decidable, no tool realizing its corresponding decision procedure has been developed. A main motivation for our work is enabling for the use of model checking, for analyzing specifications in this deontic temporal logic.
We present the technical details involved in the characterization, and prove that the model checking problem on the deontic temporal logic is correctly reduced to μ-calculus model checking. We also show that counterexamples are preserved, which is crucial for our model checking purposes. Finally, we illustrate our approach via a case study, including the verification of some properties using a μ-calculus model checker.
Araceli Acosta, Cecilia Kilmurray, Pablo F. Castro, Nazareno M. Aguirre
An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting
Abstract
This paper presents an approach to verify PLCs, a common platform to control systems in the industry. We automatically translate PLC programs written in the languages of the IEC 61131-3 standard to B models, amenable to formal analysis of safety constraints and general structural properties of the application. This approach thus integrates formal methods into existing industrial processes, increasing the confidence in PLC applications, nowadays validated mostly through testing and simulation. The transformation from the PLC programs to the B models is described in detail in the paper. We also evaluate the approach’s potential with a case study in a real railway application.
Haniel Barbosa, David Déharbe
Palytoxin Inhibits the Sodium-Potassium Pump – An Investigation of an Electrophysiological Model Using Probabilistic Model Checking
Abstract
Automatic verification techniques such as Probabilistic Model Checking (PMC) have been successfully applied in the specification and analysis of stochastic systems. Some biological systems show these characteristics, allowing PMC usage in unexpected fields. We present and analyze a probabilistic model for palytoxin toxin (PTX) effects on cell transport systems, structures which exchange ions across the plasma membrane. Several diseases are linked to their irregular behavior and their study could help drug development. The model developed in this work shows that as sodium concentration increases, PTX action enhances, suggesting that individuals with diets high in sodium are more vulnerable to PTX. An opposite effect is observed when the potassium concentration increases. PMC can help significantly in the understanding of how cell transport systems behave, suggesting novel experiments which otherwise might be overlooked by biologists.
Fernando A. F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos, Sérgio V. A. Campos
BETA: A B Based Testing Approach
Abstract
While formal methods provide ways to specify and verify software systems with mathematical accuracy, testing techniques can provide mechanisms to identify defects that were inserted in the system during its implementation. With that in mind, this paper presents an approach to generate test specifications based on a formal notation: the B-Method. Our approach is supported by a tool and uses restrictions described on a B specification, such as invariants, preconditions and conditional statements, to create unit tests for an operation. The approach uses equivalence classes and boundary value analysis techniques to partition the operation input space and relies on combinatorial criteria to select partitions to test. The approach and the tool were evaluated through a small case study using specifications for the FreeRTOS micro kernel.
Ernesto C. B. de Matos, Anamaria Martins Moreira
A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications
Abstract
SCR is a formal requirements language and method designed to detect and correct errors during the requirements phase. In this paper we start with an SCR specification, translate it into a CSP model (particularly the CSP# variant) and then apply LTL model checking on the CSP# specification to generate test vectors as counter-examples. Before the actual test vector generation, our strategy supports the verification of properties like completeness and determinism of the model; this is one of the advantages of using a process algebra for an intermediate model representation. Our strategy has been assessed by considering typical system requirements of the Aviation Industry. We compared the test vectors generated by our strategy with test vectors written manually by specialists. With respect to the examples used, our strategy has proven to be feasible and was able to generate the same test vectors.
Gustavo Carvalho, Diogo Falcão, Alexandre Mota, Augusto Sampaio
Specification Patterns for Properties over Reachable States of Graph Grammars
Abstract
Essential characteristics of the behavior of a system may be described by properties. These descriptions must be precise and unambiguous to enable verification through (semi-)automated tools. There are many appropriate mathematical languages for writing system requirements, but they are often difficult to be applied by user without a good mathematical background. Patterns for property specifications capture recurring solutions for common problems, simplifying this task. This paper presents specification patterns for properties over reachable states of graph grammars, that is, properties of complex graph structures. This proposal may be used to aid the verification of systems where states are represented as graphs.
Simone André da Costa Cavalheiro, Luciana Foss, Leila Ribeiro
Compositionality and Refinement in Model-Driven Engineering
Abstract
Model-driven engineering involves the automatic generation of software artifacts from models of structure and functionality. The use of models as ‘source code’ has implications for the notions of composition and refinement employed in the modelling language. This paper explores those implications in the context of object-oriented design: establishing a necessary and sufficient condition for a collection of classes to be treated as a component, identifying an appropriate notion of refinement for the generation process, and investigating the applicability of data and process refinement to object models.
Jim Davies, Jeremy Gibbons, David Milward, James Welch
Identifying Hardware Failures Systematically
Abstract
Critical control systems can only be used after approval of certification authorities due to safety reasons, among other aspects. Undetected failures in such systems can be catastrophic, including the loss of human lives or huge amounts of money. The safety assessment process aims to minimize such problems. But actually it still is largely dependent on human support (engineer’s experience). To decrease this human dependency, we propose a systematic hardware-based failure identification strategy. Following common practices in industry, which use Simulink diagrams to design (critical) control systems, the starting point of our proposed strategy is Simulink diagrams. The systematic identification is performed by the model checker FDR [11]. Therefore, we translate Simulink diagrams into CSP M specifications [30]. With our strategy, engineers only need to label certain Simulink elements as hardware and choose specific failure names for the generic ones our strategy provides. We illustrate our work on a simple but real case study supplied by our industrial partner EMBRAER.
André Didier, Alexandre Mota
Investigating Time Properties of Interrupt-Driven Programs
Abstract
In design of dependable software for real-time embedded systems, time analysis is an important but challenging problem due in part to the randomicity and nondeterminism of interrupt handling behaviors. Time properties are generally determined by the behavior of the main program and the interrupt handling programs. In this paper, we present a small but expressive language for interrupt-driven programs and propose a timed operational semantics for it which can be used to explore various time properties. A number of algebraic laws for the computation properties that underlie the language are established on top of the proposed operational semantics. We depict a number of important time properties and illustrate them using the operational semantics via a small case study.
Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu, Shengchao Qin
Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows
Abstract
In this paper, we present a characterization of workflows as labeled transition systems, focusing on an encoding of workflow specifications based on workflow patterns. This encoding models tasks in a convenient way, enabling us to exploit fluent linear time temporal logic formulas for capturing typical constraints on workflows. Fluents enable us to flexibly characterize the activities associated with workflow tasks, and also to easily express a wide range of constraints on workflows. Moreover, our characterization of workflows as labeled transition systems, and the use of fluent linear time temporal logic as a language to express workflow properties, allows us to employ model checking for automatically guaranteeing that a property is satisfied by a workflow, or generating violating workflow executions when such property does not hold.
We use YAWL as a language for expressing workflows. Our characterization of workflows as labeled transition systems is implemented in a tool that translates YAWL models into FSP, and then employs the LTSA tool to automatically verify properties of workflows, expressed as fluent linear time temporal logic properties, on the resulting FSP models.
Germán Regis, Nicolás Ricci, Nazareno M. Aguirre, Tom Maibaum
Composition of Model Transformations: A Categorical Framework
Abstract
Consistency management in evolving information systems is hard, for two reasons. On the one hand, large databases exist which have to be adjusted. On the other hand, many programs access those data. Data and programs all have to be synchronized in a consistent manner. It cannot be relied upon, however, that no running processes exist during such a migration. Consequently, a restructuring of an information system needs to take care of the migration of object-oriented systems comprising data, programs, and processes. This co-evolution together with the notion of model transformation and instance migration has been introduced in earlier papers. This paper builds upon this exploratory work and analyses under which circumstances composed model transformations are compatible with composed instance migrations. We develop the notion of shortcut paths and show that composition is possible if shortcut paths are reflected by the underlying model transformations.
Christoph Schulz, Michael Löwe, Harald König
Verification Rules for Exception Handling in Eiffel
Abstract
The Eiffel exception mechanism supports two methodological aspects. First, a method specification by a pre- and postcondition also determines when the method exits exceptionally, namely when the stated postcondition cannot be satisfied. Secondly, the rescue and retry statements combine catching an exception with a loop structure, thus requiring a dedicated form of correctness reasoning. We present verification rules for total correctness that take these two aspects into account. The rules handle normal loops and retry loop structures in an analogous manner. They also allow the Eiffel’s mechanism to be slightly generalized. The verification rules are derived from a definition of statements by higher-order predicate transformers and have been checked with a theorem prover.
Emil Sekerinski, Tian Zhang
A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications
Abstract
Formal dynamic analysis of Message Passing Interface (MPI) programs is crucially important in the context of developing HPC applications. Existing dynamic verification tools for MPI programs suffer from exponential schedule explosion, especially when multiple non-deterministic receive statements are issued by a process. In this paper, we focus on detecting message-orphaning deadlocks within MPI programs. For this analysis target, we describe a sound heuristic that helps avoid schedule explosion in most practical cases while not missing deadlocks in practice. Our method hinges on initially computing the potential non-deterministic matches as conventional dynamic analyzers do, but then including only the entries which are found relevant to cause a refusal deadlock (essentially a macroscopic-view persistent-set reduction technique). Experimental results are encouraging.
Subodh Sharma, Ganesh Gopalakrishnan, Greg Bronevetsky
Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions
Abstract
This work presents a complete formalization of Alternating-time Temporal Logic (ATL) and its semantic model, Concurrent Game Structures (CGS), in the Calculus of (Co)Inductive Constructions, using the logical framework Coq. Unlike standard ATL semantics, temporal operators are formalized in terms of inductive and coinductive types, employing a fixpoint characterization of these operators. The formalization is used to model a concurrent system with an unbounded number of players and states, and to verify some properties expressed as ATL formulas. Unlike automatic techniques, our formal model has no restrictions in the size of the CGS, and arbitrary state predicates can be used as atomic propositions of ATL.
Dante Zanarini, Carlos Luna, Luis Sierra
Backmatter
Metadaten
Titel
Formal Methods: Foundations and Applications
herausgegeben von
Rohit Gheyi
David Naumann
Copyright-Jahr
2012
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-33296-8
Print ISBN
978-3-642-33295-1
DOI
https://doi.org/10.1007/978-3-642-33296-8

Premium Partner

    Bildnachweise