What types of applications have you used model checking for? What model checking tool did you use? How would you summarize your experience w/ the technique, specifically in evaluating its effectiveness in delivering higher quality software? In the course of my studies, I had a chance to use Spin, and it aroused my curiosity as to how...
Beyond some valid reasons not to use a new tool such as support of legacy code, no in-house SPARKAda knowledge base, why hasn't SPARKAda caught on? It seems like a very sound tool for many projects requiring high reliability, so I don't understand why its not so common. I would be more comfortable knowing that the avionics software that ...
So... I teach formal methods in software engineering. I also teach "agile methodologies". Most people seem to think this is contradictory. I think it makes a lot of sense... I also work for a company, where we need to actually get things done :) While I can apply my earned skill points on "specification" in a day-to-day basis, my collea...
Our client wants us to build a web-based, rich internet application for gathering software requirements. Basically it's a web-based case tool that follows a specific process for getting requirements from stakeholders. I'm the project manager and we're still in the early phases of the project. I've been thinking about using formal meth...
Here's a sort of odd question. I'm in the process of writing a book on learning to program using formal methods, and I'm going to target it toward people with some programming experience. The idea is to teach them to be high-quality programmers. The basic notation is going to be from Dijkstra's Discipline of Programming, along with so...
I've found that my (USA) professors recoil with a near-disgust when I ask them about how to pursue a career in Formal Methods programming. They say, "Oh, that stuff! That stuff is anal. You don't need that European POS to get a job." I'm sure I'll get a job without it, but Formal Methods interests me so much that I bet I'd like to make...
Hello everyone, I'm a software developer interested in information retrieval. Currently I'm working on my 3rd search engine project and am VERY frustrated about the amount of boilerplate code that is written again and again, with the same bugs, etc. Basic search engine is a very simple beast that could be described in a formal language ...
I have been interested in formal methods for some time. I have used formal methods to reason about some very specific sub-areas of a few projects I have been working on. I was never able to convince other team members to try the same let alone specify an entire domain with a formal method. One method I have found particularly interesti...
I want to be able to split a big test to smaller tests so that when the smaller tests pass they imply that the big test would also pass (so there is no reason to run the original big test). I want to do this because smaller tests usually take less time, less effort and are less fragile. I would like to know if there are test design patte...
i am working on checking model consistency of software. to do this i need to write linear temporal logic for UML 2.0 sequence diagram. if any body have any other tool for the same please response as soon as possible. I will be very obliged to you. i have found charmy tool have plugin for the same. Does anybody have source code for charmy...
When using formal aspects to create some code is there a generic method of determining a loop invariant or will it be completely different depending on the problem? ...
I came upon the Curry-Howard Isomorphism relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept there exists a precise analogue in formal logic, and vice versa. Here's a "basic" list of such analogies, off the top of my head: program/defini...
Hi ! I remember reading something about a formal specification language for C a while ago, but I can not find it now that I need it. It was inspired by JML, using as far as I saw the same syntax. The only reference to it I found is a paper, but what I am talking about was more polished than that. If this rings a bell to you... If n...
I'm looking at the requirements for automated software verification, i.e. a program that takes in code (ordinary procedural code written in languages like C and Java), generates a bunch of theorems saying that each loop must eventually halt, no assertion will be violated, there will never be a dereference of a null pointer etc., then pas...