TS News

News

SYNTCOMP 2015
2015-10-30 Adam Walker wins the synthesis competition again this year in his category Sequential realizability More:

Seminar 2015-10-14: Nickolai Zeldovich - Using Crash Hoare Logic for Certifying the FSCQ File System
This talk will describe FSCQ, the first file system with a machine-checkable proof (using Coq) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.

Seminar 2015-10-14: Nickolai Zeldovich - Using Crash Hoare Logic for Certifying the FSCQ File System

This talk will describe FSCQ, the first file system with a machine-checkable proof (using Coq) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.

2015-09-01 Google PhD fellowship
Congratulations to PhD student Qian Ge who has won a Google PhD fellowship with Research Proposal Title: Low Overhead Operating System Mechanisms for Eliminating Microarchitectural Timing Side Channels

Seminar 2015-08-25: Huan Nguyen on Rule-Based Extraction of Goal-Use Case Models from Text
Goal and use case modeling has been recognized as a key approach for understanding and analyzing requirements. However, in practice, goals and use cases are often buried among other content in requirements specifications documents and written in unstructured styles. It is thus a time-consuming and error-prone process to identify such goals and use cases. In addition, having them embedded in natural language documents greatly limits the possibility of formally analyzing the requirements for problems. To address these issues, we have developed a novel rule-based approach to automatically extract goal and use case models from natural language requirements documents. Our approach is able to automatically categorize goals and ensure they are properly specified. We also provide automated semantic parameterization of artifact textual specifications to promote further analysis on the extracted goal-use case models. Our approach achieves 85% precision and 82% recall rates on average for model extraction and 88% accuracy for the automated parameterization.

Seminar 2015-08-25: Huan Nguyen on Rule-Based Extraction of Goal-Use Case Models from Text

Goal and use case modeling has been recognized as a key approach for understanding and analyzing requirements. However, in practice, goals and use cases are often buried among other content in requirements specifications documents and written in unstructured styles. It is thus a time-consuming and error-prone process to identify such goals and use cases. In addition, having them embedded in natural language documents greatly limits the possibility of formally analyzing the requirements for problems. To address these issues, we have developed a novel rule-based approach to automatically extract goal and use case models from natural language requirements documents. Our approach is able to automatically categorize goals and ensure they are properly specified. We also provide automated semantic parameterization of artifact textual specifications to promote further analysis on the extracted goal-use case models. Our approach achieves 85% precision and 82% recall rates on average for model extraction and 88% accuracy for the automated parameterization.

Seminar 2015-08-20: Florian Daniel; Recommendation and Weaving of Reusable Mashup Model Patterns for Assisted Development
Mashups are composite applications developed starting from reusable data, application logic and/or user interfaces, for example, sourced from the Web. Mashup tools are IDEs for mashup development that aim to ease mashup development, typically via model-driven development paradigms. This talk reports on recent research outcomes that aim to answer one of the problems proper of the mashup domain, that is, the lack of modeling expertise. This kind of knowledge is generally neither intuitive nor standardized across different tools, and the consequent lack of modeling expertise affects both skilled programmers and end-user programmers alike. The talk shows how to effectively assist the users of mashup tools with contextual, interactive recommendations of composition knowledge in the form of reusable mashup model patterns. It describes the design and performance study of three different recommendation algorithms and a pattern weaving approach for the one-click reuse of model patterns inside model-driven mashup tools. It discusses the implementation of suitable pattern recommender plugins for three different mashup tools and demonstrates via user studies that recommending and weaving contextual mashup model patterns significantly reduces development times in all three cases. The approach is of general nature and can easily be tailored to other model-driven development environments.

Seminar 2015-08-20: Florian Daniel; Recommendation and Weaving of Reusable Mashup Model Patterns for Assisted Development

Mashups are composite applications developed starting from reusable data, application logic and/or user interfaces, for example, sourced from the Web. Mashup tools are IDEs for mashup development that aim to ease mashup development, typically via model-driven development paradigms. This talk reports on recent research outcomes that aim to answer one of the problems proper of the mashup domain, that is, the lack of modeling expertise. This kind of knowledge is generally neither intuitive nor standardized across different tools, and the consequent lack of modeling expertise affects both skilled programmers and end-user programmers alike. The talk shows how to effectively assist the users of mashup tools with contextual, interactive recommendations of composition knowledge in the form of reusable mashup model patterns. It describes the design and performance study of three different recommendation algorithms and a pattern weaving approach for the one-click reuse of model patterns inside model-driven mashup tools. It discusses the implementation of suitable pattern recommender plugins for three different mashup tools and demonstrates via user studies that recommending and weaving contextual mashup model patterns significantly reduces development times in all three cases. The approach is of general nature and can easily be tailored to other model-driven development environments.

Show older articles

Trustworthy Systems

News