Sharpen the Saw for Computer Scientists

It’s december and a new year will start a few days from now. It’s that time of the year where we think of thinks we want to achieve or do more often the next year. Often theses things include sports, losing weight or spending more time with loved ones.
These are all valid and important new years resolutions and you should go for them. But there is one more thing, let’s think about how we can sharpen our saws to become better at our work. This list is primarily intended for computer scientists and software engineers, developers and architects but probably can be adapted for other professions as well.

Here’s some ideas, some mine, some are inspired by a similar post of Scott Hanselman:

  • Set-aside time, like one or two hours per week, to read technical books or papers related to your field of work.
  • Set-aside time to read one technical paper or book that is not related to your field of work per month.
  • Listen to podcasts, or watch screencasts about new technologies and approaches.
  • Attend conferences and talks and most importantly try to ask questions or at least write down questions and try to figure out the answer for your self.
  • Discuss problems with your co-workers, you might be surprised how much you can learn from a good discussion.
  • Help others, sometimes there is no better and satisfactory way than helping someone to solve a technical problem.
  • Try something new! Whether it is a new programmin language, new software architecting tool or a new software process model you’ll never know when you need it.

Quantitative Safety Analysis of UML Models

My master’s thesis is now available online here.

Abstract

When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.

My first workshop paper

I recently finished my bachelor thesis and will present a part of it as a short paper at the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) in L’Aquila, Italy.

Simulink Design Verifier vs. SPIN – A Comparative Case Study Florian Leitner and Stefan Leue

Keywords
State Space Exploration, Matlab Simulink, SPIN, Automotive Software

Abstract
An increasing number of industrial strength software design tools come along with verification tools that offer some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Verifier and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.