undefined | Better HN

0 pointsnickpsecurity9y ago0 comments

UML specs them at an abstract level. You build them in code or HDL's. Few, formal methods can do both. Generally, you prove properties in the abstract in one and correspondence with the other. Code-level proofs only came online only in past 5-10 years or so in a subfield 40 years old.

So, UML would let you specify data and behavior then confirm properties about them, catch inconsistencies in requirements, or aid integrations. SysML is used for this in industry with verification results in academia even for UML as I showed. So, it's reality rather than theory even if you or I think better methods exist. I'll take a combo of Z, B, CSP, and/or Statecharts over UML anyday. Coq and HOL if I was specialist enough.

0 comments

nickbauman9y ago

Not saying you're wrong: At the end of the day to the degree that any of these methods (UML, TLA+, whatever) formally prove correctness is the same degree that they gain the features of a turing-complete programming language. Which comes back to the notion design is the source code itself and represents the majority of the work. The compiler or interpreter is the "construction" phase of the project.

j / k navigate · click thread line to collapse

0 pointsnickpsecurity9y ago0 comments

0 comments

nickbauman9y ago

j / k navigate · click thread line to collapse