Statecharts are good stuff. It was not mentioned in the article, but there’s a recent W3C XML standard for representing them now, which might be handy to those interested in adapting model-checking tools to this purpose.
Qt is working on some nice statechart-based tools too. Glad to see the formalism being rescued from the UML bog. Who knows, some day industry may even catch up to academic work that Harel and friends were doing with “Live Sequence Charts” in the early 2000s.
The Tenix Data Diode used them for an EAL7 evaluation IIRC. There were CASE tools for them. They’re useful and easy to learn being the best things about them.
I was going to point out there were test generation, model-checking, and verification tools for Statecharts. Googling them made me find more I hadn’t seen, including two on specifying UI’s for web apps. So, I’ll just submit them this week. :) Probably batch the lesser ones into a comment in a submission of more interesting ones.
In order to add a logout feature we had to add four more edges. This quickly gets untenable.
I didn’t understand why this is really an issue though. It feels like increasing the size of a for-loop to me. I do like the nested representation and use nesting quite a bit.
I didn’t understand why this is really an issue though. It feels like increasing the size of a for-loop to me.
Adding additional edges to an FSM makes it visually harder to parse. Since the point of an FSM is to convey information to humans, making it harder to parse makes it less useful as a specification.
When you started drawing automata, I thought you were going to go the linear temporal logic or Computation tree logic route.
My main spec language is TLA+, which can express the more sophisticated properties quite easily. The problem is that it doesn’t handle subtyping at all, when representing nested states as subtypes is a really elegant way to encode the spec.
The reason Alloy can’t handle things like deadlocks or liveness is because it’s carefully designed to be as user-friendly as possible. Among other things, that means checking specs really really fast, which means using a SAT solver, which means no infinite traces. We’ve been thinking of changing it to use an SMT solver, but right now the costs are just too high to make switching worth it.
There is, and I’m slowly working my way through it to write a blog post. THis is way more interesting as an introduction to model checking compared to the usual examples of the rower with the dog,duck, and sack of corn.
“But it’s more widely useful than that. This is especially important for UI.”
One thing I hated about some apps’ UI’s is they would lock up in a modal dialog that kept repeating or not let me press a button even when it was next step. I’d definitely appreciate developers stopping stuff like that when building software I use. Maybe tools like this could help.
“There’s also some properties we can’t easily verify in Alloy, such as finding deadlocks. “
Have you not checked out Electrum yet or did I not send it to you? That Alloy extension lets one check temporal properties. I know it can handle safety and liveness. Part of a Dijkstra spec mentioned deadlocks. Seems like the thing to try if wanting Alloy + temporal checks. Here’s a tutorial.
“FSMs share a lot in common with deterministic-finite automata, which is an important concept in CS. The main difference is in the use-case: DFAs are motivated by “which regular languages does this accept”, while FSMs are motivated by “is our specification consistent?””
A DFA is a FSM. In OOP, it would be one of the child classes. Other main one is NFA. The Automata Theory and FSM articles on Wikipedia have a lot of good detail on them.
Have you not checked out Electrum yet or did I not send it to you? That Alloy extension lets one check temporal properties. I know it can handle safety and liveness. Part of a Dijkstra spec mentioned deadlocks. Seems like the thing to try if wanting Alloy + temporal checks. Here’s a tutorial.
Oh, you definitely sent it to me! It’s not core Alloy though, so I didn’t include it.
Fun fact: I was invited to talk at the Future of Alloy conference back in May. One of the session blocks was everybody sharing their Alloy extensions: Electrum, DASH, HaiQ, etc. One of the goals of the conf was to see if any of these should supersede Alloy and/or if we should build in a simplified extension mechanism. Our conclusion was to stay conservative for now.
Oh OK. Thanks for the update. That does indicate one might make extensions pluggable like DSL’s in some languages. They might already but I’m thinking have a few for different use cases.
Statecharts are good stuff. It was not mentioned in the article, but there’s a recent W3C XML standard for representing them now, which might be handy to those interested in adapting model-checking tools to this purpose.
Qt is working on some nice statechart-based tools too. Glad to see the formalism being rescued from the UML bog. Who knows, some day industry may even catch up to academic work that Harel and friends were doing with “Live Sequence Charts” in the early 2000s.
The Tenix Data Diode used them for an EAL7 evaluation IIRC. There were CASE tools for them. They’re useful and easy to learn being the best things about them.
I was going to point out there were test generation, model-checking, and verification tools for Statecharts. Googling them made me find more I hadn’t seen, including two on specifying UI’s for web apps. So, I’ll just submit them this week. :) Probably batch the lesser ones into a comment in a submission of more interesting ones.
@hwayne I gotta say, you always post excellent stuff. Bravo.
Thank you!
I didn’t understand why this is really an issue though. It feels like increasing the size of a for-loop to me. I do like the nested representation and use nesting quite a bit.
When you started drawing automata, I thought you were going to go the linear temporal logic or Computation tree logic route.
This is from memory and Wikipedia and I could be getting it very wrong:
exists(always(not Student) and eventually(Answers))
exists(eventually(Logout and eventually(Login)))
(Not really an example.)
for all states s, always(next(Summary) implies eventually(s)) and always(next(s) implies eventually(Summary))
“You can reach everything from Summary and you can reach Summary from everything.”
Adding additional edges to an FSM makes it visually harder to parse. Since the point of an FSM is to convey information to humans, making it harder to parse makes it less useful as a specification.
My main spec language is TLA+, which can express the more sophisticated properties quite easily. The problem is that it doesn’t handle subtyping at all, when representing nested states as subtypes is a really elegant way to encode the spec.
The reason Alloy can’t handle things like deadlocks or liveness is because it’s carefully designed to be as user-friendly as possible. Among other things, that means checking specs really really fast, which means using a SAT solver, which means no infinite traces. We’ve been thinking of changing it to use an SMT solver, but right now the costs are just too high to make switching worth it.
Oh, right. I forgot Alloy isn’t TLA+. Thanks.
From this I got to Baugh and Altuntas, “Formal Methods and Finite Element analysis”…
Which is blowing my mind right now.
That was pretty interesting. You should submit that Wednesday or Thursday if there’s a non-paywalled copy.
There is, and I’m slowly working my way through it to write a blog post. THis is way more interesting as an introduction to model checking compared to the usual examples of the rower with the dog,duck, and sack of corn.
“But it’s more widely useful than that. This is especially important for UI.”
One thing I hated about some apps’ UI’s is they would lock up in a modal dialog that kept repeating or not let me press a button even when it was next step. I’d definitely appreciate developers stopping stuff like that when building software I use. Maybe tools like this could help.
“There’s also some properties we can’t easily verify in Alloy, such as finding deadlocks. “
Have you not checked out Electrum yet or did I not send it to you? That Alloy extension lets one check temporal properties. I know it can handle safety and liveness. Part of a Dijkstra spec mentioned deadlocks. Seems like the thing to try if wanting Alloy + temporal checks. Here’s a tutorial.
“FSMs share a lot in common with deterministic-finite automata, which is an important concept in CS. The main difference is in the use-case: DFAs are motivated by “which regular languages does this accept”, while FSMs are motivated by “is our specification consistent?””
A DFA is a FSM. In OOP, it would be one of the child classes. Other main one is NFA. The Automata Theory and FSM articles on Wikipedia have a lot of good detail on them.
Oh, you definitely sent it to me! It’s not core Alloy though, so I didn’t include it.
Fun fact: I was invited to talk at the Future of Alloy conference back in May. One of the session blocks was everybody sharing their Alloy extensions: Electrum, DASH, HaiQ, etc. One of the goals of the conf was to see if any of these should supersede Alloy and/or if we should build in a simplified extension mechanism. Our conclusion was to stay conservative for now.
Oh OK. Thanks for the update. That does indicate one might make extensions pluggable like DSL’s in some languages. They might already but I’m thinking have a few for different use cases.