What is your experience with software model validation?

  • What types of applications did you use model validation for?
  • What model validation tool did you use?
  • How would you generalize your experience and technology, in particular, evaluating its effectiveness in providing better software?

In the course of my research, I had the opportunity to use Spin , and this aroused my curiosity as to how the model validation continues and how valuable organizations coming out of it are. In my experience, I worked on business applications, where (naturally) there is no need to apply formal verification to logic. I would really like to learn about how SO tests experience and thoughts on this topic. Will model testing ever become the more widely used evolving practice we should have in our toolkit?

+5
source share
5 answers

, , , Spin SMV. , , , SMV .

, , , -, ( "" ). , Spring Framework WebFlow, XML , , , - , SMV, ( ).

, , , , .

+3

, . SPIN, UPPAL, Java Pathfinder, PVS Bogor. . , . , .

? , , , ( ) , , . , , - , .

+2

?

Java Path Finder (, ) ( ). (, NotNull) Java (-) - .

?

Java Path Finder ( ). , NASA .

, , ?

( ). , , , , ..

+2

SPIN concurrency . , .

, "SPIN for Dummies"? " SPIN Model Checker" -.

0

, State Exploring Assembly Model Checker.

/ , A * , (, -,...)

Java Pathfinder ++. (, GCC )

But in our experience, this technology will not be used in business applications in the near future due to problems associated with the GUI, the work necessary to create an initial test environment and huge hardware requirements. (You need a lot of RAM and disk space due to the giant state space)

0
source

All Articles