Reputation: 460 Architect
- Active Members
- Active Posts:
- 817 (0.33 per day)
- 17-June 08
- Profile Views:
- Last Active:
- Mar 25 2015 08:56 AM
- OS Preference:
- Favorite Browser:
- Favorite Processor:
- Who Cares
- Favorite Gaming Platform:
- Who Cares
- Your Car:
- Who Cares
- Dream Kudos:
Posts I've Made
Posted 20 Mar 2015It's actually a question asking for you to clarify what did you mean by "formal modeling languages" and "code-level verification". The myth was your assumption on what motivated my question.
On rereading my post, I realize this may sound rude. Sorry if it does. I meant no offense.
No offense taken. Sorry I misunderstood what you were asking. I just meant that I looked at methods and notations that dealt more with higher-level abstractions, such as modeling the overall design of a system, as opposed to techniques for verifying implementations at the code level. So more things like applying VDM or Z to system specifications as opposed to analyzing source code. Nothing terribly deep - I probably could have phrased it better.
This apparently says that VDM can model a system at a higher level and then drop to code level verification. Is this true? Can VDM be used on all levels? Am I misreading it?
Your understanding is correct. I don't claim to be an expert on VDM, and I didn't get too deep into the refinement part of it, but it does include methods for refining your models from higher to lower level. And yes, you can go all the way down to the code level if you really want to. Of course, as Skydiver was getting at, the semantics of a low-level VDM specification will not necessarily map to your implementation language, so you'd just be verifying the logic of your program, not the actual implementation. But depending on your goals, that's not necessarily a problem.
EDIT: Or maybe, if the model have been proven correct, we can generate correct code without verification? True? False?
If you have a sufficiently detailed model, this is theoretically possible. At the lowest level, an explicit VDM specification is essentially equivalent to source code. And there are "model animators" that will allow you to "execute" a specification like a program. I seem to recall that Overture could do model animation, though it was limited to explicit specifications. It's been a while, though, so I'm not certain.
As far as actually generating code from a specification, I've only read about it. I have no experience with it so I don't know if there are any tools available to do it or what their quality is.
I chose C++ for this and I was looking around for a formal method that can enable me to enter a less buggy beta testing stage. I think I can achieve this with VDM++. Is this true?
Maybe. Using formalism can help you to think more rigorously about the program you're building and give you another tool to analyze it. This can help you verify that your program covers all your requirements, that you haven't missed things in the design, that your logic is correct, etc. My own experience, and what I've read in case studies, is that they can help you find bugs before you've written them in the implementation language. But as I said in a previous post, formalism is just another tool and how much value you get out of it will depend on how you use it. If this is your first project with VDM++, it might be useful, but because the learning curve is steep you shouldn't expect huge quality improvements right away.
Maybe VDM-SL is well suited for such a project. Is it?
I don't know. It really depends on what you're trying to accomplish. Actual execution speed is more of a low-level, implementation-dependent thing, so I wouldn't necessarily expect a notation like VDM-SL to be too helpful in analyzing that (though to be honest, I haven't looked into that at all). Now if you wanted to use VDM to model different implementations and make sure that they're still behaving correctly, that's a different story. I can see VDM working well for something like that.
Is there a drawback on using formal methods for developing those two projects, other than the learning time I have to take?
Well, it really all comes down to time.
First, there's the learning curve. For most formal methods, it's pretty steep, even if you already have the mathematical background for them. In addition to the notation, it's kind of a different way of thinking. As one article I read put it, writing formal specifications is a different skill set than writing code. It's a new way of doing things that you'll have to integrate into your development process.
Second, there's the time spent actually working with the formalism. Experienced formal methods practitioners do the formal analysis and get the project done in the same or less time than without it, because the extra up-front analysis translates to fewer issues during implementation. However, if you're not experienced, this may not be the case. The formalization will probably take you longer; you may find holes or errors in your analysis and have to revisit it later in the development cycle; you may do too much formalization and end up doing a lot of analysis that just isn't that useful.
In any event, I expect the only thing you stand to lose is time. If you're not experienced, then it's debatable how much using VDM will increase the quality of your software, but I doubt it would make it any worse. The only risk is that you end up taking more time than you'd like to complete the project. Just make sure your expectations are reasonable. If you're looking for immediate results on these projects, you may be disappointed. I would look at these projects more as "pilot programs" to help you learn VDM so you can use it to better effect in the future. That's one of the big lessons from the literature - learning formal methods is a long-term investment.
Posted 19 Mar 2015As a rule of thumb, you can apply the same organizational principles to test code that you do to your application code. It may be a common pattern, but there's no law that says you have to have exactly one test class per application class. If the test class is getting too unwieldy, then by all means go ahead and break it up. You could also do one test class per method, or one for each logical feature, or something else entirely - whatever makes the most sense for your case. The exact scheme you use isn't that critical so long as the organization is consistent and it's easy to figure out where a particular test would be located.
However, you can also look at it from the other direction. Maybe the huge test class is an indication of other problems. Does the class under test really need to be that big? Maybe the solution is to refactor your application class into multiple smaller classes, in which case the test organization would take care of itself. (Not that I know one way or the other - I'm just playing devil's advocate here.)
Posted 18 Mar 2015What is the difference?
This is actually myth number 2 in Hall's 7 Myths of Formal Methods. The term "formal methods" encompasses a number of techniques for dealing with systems mathematically. Code verification is just one of those. I looked at modeling systems at a higher level using what is often referred to as a formal specification. The idea is that rather than proving properties about a program in terms of lines of code, you can model a larger system using mathematical entities (often based on predicate logic and set theory) and verify properties of it at that level. At that level, the formal models are more about validating the design of the system and not so much about the low-level implementation details.
QuoteI then looked into VDM. It looks like something similar to what Prof. Gries taught in his book, so it grabbed my attention.
I can relate to that. I started out looking mainly at Z and Object-Z, but ended up switching to VDM++. It just felt more natural to me. It also didn't hurt that it was easier to write the specifications, as the Z notation uses some funky characters and, at least at the time, required a special editor unless you wanted to write in LaTeX, whereas VDM++ had a handy ASCII-only version.
QuoteCould you recommend books and/or websites about VDM?
Two of the books that I used are Systematic Software Development Using VDM by Cliff Jones (1990) and Validated Designs for Object-oriented Systems by Fitzgerald, Larsen, et al. (2004). I would also definitely take a look at the website for Overture. It's an open-source toolset, built on top of Eclipse, for working with VDM and VDM++. It's been a while since I worked with it, but I understand it's come a long way since then. The website also has a lot of good information on VDM and links to other books.
Posted 18 Mar 2015If it's not obvious, I've been a skeptic when I first heard of formal methods many years ago.
The main reason my skepticism is is that somebody trying to verify the correctness of a program has to not only verify the correctness at the problem domain level, but they will also have to do the same down at the implementation language level, and perhaps at the machine language level? Compilers do have bugs. Have the compilers been proven to be correct? How about the libraries used? Have they been proven correct?
Your skepticism is not unwarranted - formal methods have definitely been over-sold in some circles. It should be too obvious to bear repeating, but formal methods cannot guarantee bug-free software. Nothing can. That was actually the first item in Anthony Hall's list of 7 Myths of Formal Methods. But just because formal methods have limitations doesn't mean they have no value. They're just another tool in the toolbox. They can be a useful way to increase confidence in the correctness of a system, but like any tool you need to understand their strengths and weaknesses in order to get good results. They are not a silver bullet.
Posted 16 Mar 2015Back in 1989, when I was coursing my last year in college, I had the honour to be a student of Professor David Gries. Math department on RUM Puerto Rico invited him to teach a course titled "The Science of Programming".
I used the same book for a class on Formal Methods in grad school. It's fascinating stuff. In fact, I ended up doing my thesis on how formal methods are used in industry, though I looked more at formal modeling languages (I focused on VDM++) as opposed to code-level verification.
Betsemes said:I'm under the impression that programming is taught and done without formal verification, but I also got the impression that the subject has been developed much further.
Your impression would be correct on both counts.
Formal methods never really made it into the mainstream. Many (most?) programmers have never studied them in any form and are not even aware that the field exists. They are used in various ways and to various degrees in parts of the software industry, such as those dealing with safety- or security-critical systems, but they're not really on the radar of most software shops.
As you would expect, there has been a lot of new developments since Gries published his book and there was a lot of other stuff going on at the time that he didn't cover. I can't really recommend any specific books or websites - it all depends on what you're interested in. There are a lot of different methods and notations that have been developed and much of the published material is specific to a particular method or technique. I guess the best I could suggest is to start with the Formal Methods Wiki, figure out what looks interesting to you, and go from there.
I'll have to dig into the details, but off the top of my head, so if my program invokes undefined behavior, conceptually that seems like a failure to me, but how do I write a verification spec that says it is a failure? If the very nature of the undefined behavior it may give a successful result.
You wouldn't do that. As soon as you say "it invoked undefined behavior", all bets are off - you can't reason mathematically about something that doesn't have a definition. The point of formally verifying a program is to avoid invoking undefined behavior. Typically, the spec would define what you want the program to do, e.g. "given that X is true before the code runs, Y should be true after it runs." Verification would then consist of constructing a formal proof that, if X is true, the formal definitions of the program statements imply that Y will necessarily be true. If there is any undefined behavior in your program, it'll show up in the math and you won't be able to prove Y.
- Member Title:
- Resident Curmudgeon
- 37 years old
- August 16, 1977
- Brockport, NY
- On the technical front, I'm interested in software design methods, formal modeling, database theory, etc.. In more general terms, I like to play the piano, study philosophy, and work in my garden.
- Years Programming:
- Programming Languages:
- PHP, Python, VB.NET/6, C#, SQL, ActionScript (mostly FLEX), and whatever other stuff I've worked with that I feel like including today.
- Website URL: