* What is SPARK about? @ 2010-06-11 20:32 Claude 2010-06-11 23:01 ` Simon Wright 2010-06-12 8:30 ` Phil Thornley 0 siblings, 2 replies; 12+ messages in thread From: Claude @ 2010-06-11 20:32 UTC (permalink / raw) Ada is a formal language to software engineering. What is SPARK about? I means since SPARK is restricted to the best of Ada, is SPARK better than Ada to resolving complex engineering applications, or SPARK a better choice than C/C++ to address leaner systems? (in terms of compliance to early drafts of DO-178C - certification levels C to A). Indeed, the successful applications of SPARK bring to results that are rather difficult to compare. “The formal design of Tokeneer ID Station (TIS) shows the TIS system to be a purely sequential system.” - (INFORMED design, at section 2.2, Identification of the SPARK boundary) “We believe part of the success of proof on SHOLIS is due to the simple system architecture. … Some large-scale SPARK reasoning are also needed, including support for abstract proof, before the technology can be extensively used at the highest level of large systems.” - (Is Proof More Cost Effective Than Testing – Section 8, Summary). Beyond any theory or academic project, 10 years later, from all the past SPARK projects’ experiences, does it happen that SPARK can address “purely sequential systems” or that SPARK “can be extensively used at the highest level of large systems”? Claude ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-11 20:32 What is SPARK about? Claude @ 2010-06-11 23:01 ` Simon Wright 2010-06-11 23:17 ` Yannick Duchêne (Hibou57) 2010-06-12 8:30 ` Phil Thornley 1 sibling, 1 reply; 12+ messages in thread From: Simon Wright @ 2010-06-11 23:01 UTC (permalink / raw) Claude <claude.defour@orange.fr> writes: > I means since SPARK is restricted to the best of Ada The SPARK toolset supports a subset of Ada that it can reason about. As the SPARK toolset has become more capable (ie, "we" have discovered ways of programming the machine to reason about more of Ada), so the supported subset has got larger to match. As an example, I'm pretty sure SPARK doesn't handle generics; so that rules out the Container library. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-11 23:01 ` Simon Wright @ 2010-06-11 23:17 ` Yannick Duchêne (Hibou57) 2010-06-12 12:16 ` Peter C. Chapin 0 siblings, 1 reply; 12+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-06-11 23:17 UTC (permalink / raw) Le Sat, 12 Jun 2010 01:01:51 +0200, Simon Wright <simon@pushface.org> a écrit: > As an example, I'm pretty sure SPARK doesn't handle generics; so that > rules out the Container library. I did not tried it yet, so I will not any about the present state (I’ve just noticed it support the syntax). What is sure, is that support (or better support) for generic is planed for the futur... and is already present in SPARK Pro (if I'm not wrong). -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-11 23:17 ` Yannick Duchêne (Hibou57) @ 2010-06-12 12:16 ` Peter C. Chapin 0 siblings, 0 replies; 12+ messages in thread From: Peter C. Chapin @ 2010-06-12 12:16 UTC (permalink / raw) Yannick Duchêne (Hibou57) wrote: > I did not tried it yet, so I will not any about the present state (I’ve > just noticed it support the syntax). What is sure, is that support (or > better support) for generic is planed for the futur... and is already > present in SPARK Pro (if I'm not wrong). Aside from one special case, generics are not yet in SPARK Pro. I understand that some (reasonable) level of support for generics is planned for a future release, however. Disclaimer: I'm not an Altran Praxis employee. I only know what I've heard elsewhere. Peter ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-11 20:32 What is SPARK about? Claude 2010-06-11 23:01 ` Simon Wright @ 2010-06-12 8:30 ` Phil Thornley 2010-06-12 18:09 ` Claude 1 sibling, 1 reply; 12+ messages in thread From: Phil Thornley @ 2010-06-12 8:30 UTC (permalink / raw) On 11 June, 21:32, Claude <claude.def...@orange.fr> wrote: > Ada is a formal language to software engineering. > > What is SPARK about? SPARK is an annotated sublanguage of Ada, intended for use in high- integrity applications. An important property of the language is that it is unambiguous - every valid SPARK program, when compiled by a conforming Ada compiler, has one and only one meaning. Therefore it becomes practicable to reason about the behaviour of a SPARK program based solely on the analysis of the program text. > > I means since SPARK is restricted to the best of Ada, is SPARK better > than Ada to resolving complex engineering applications, or SPARK a > better choice than C/C++ to address leaner systems? (in terms of > compliance to early drafts of DO-178C - certification levels C to A). > > Indeed, the successful applications of SPARK bring to results that are > rather difficult to compare. > > “The formal design of Tokeneer ID Station (TIS) shows the TIS system > to be a purely sequential system.” - (INFORMED design, at section > 2.2, Identification of the SPARK boundary) Support for concurrent programs (RavenSPARK) was added in 2003. > > “We believe part of the success of proof on SHOLIS is due to the > simple system architecture. … > Some large-scale SPARK reasoning are also needed, including support > for abstract proof, before the technology can be extensively used at > the highest level of large systems.” - (Is Proof More Cost Effective > Than Testing – Section 8, Summary). Support for abstract proof was added in 2000. > > Beyond any theory or academic project, 10 years later, from all the > past SPARK projects’ experiences, does it happen that SPARK can > address “purely sequential systems” or that SPARK “can be extensively > used at the highest level of large systems”? An example of a large, concurrent SPARK program is iFACTS - described by the UK National Air Traffic Service as "the biggest change in air traffic control since radar". > > Claude Cheers, Phil ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-12 8:30 ` Phil Thornley @ 2010-06-12 18:09 ` Claude 2010-06-12 19:27 ` Yannick Duchêne (Hibou57) 2010-06-13 5:37 ` J-P. Rosen 0 siblings, 2 replies; 12+ messages in thread From: Claude @ 2010-06-12 18:09 UTC (permalink / raw) On Jun 12, 1:30 am, Phil Thornley <phil.jpthorn...@gmail.com> wrote: > On 11 June, 21:32, Claude <claude.def...@orange.fr> wrote: > > > Ada is a formal language to software engineering. > > > What is SPARK about? > > SPARK is an annotated sublanguage of Ada, intended for use in high- > integrity applications. Annotations (Ada comments) and Ada source code compose the SPARK semantic, which shall fly together on the SPARK tools in order to determine and discharge any Verification Condition. (Static analysis completeness is the SPARK programming goal). (Ada’s generic and variant records are within static analysis’s capabilities but still on the SPARK “road map”) > An important property of the language is that it is unambiguous - > every valid SPARK program, when compiled by a conforming Ada compiler, > has one and only one meaning. Ada source code (constrained to be unambiguous, from SPARK static analysis) shall fly alone on the Ada compiler, like the Ada executable will on the target system. (Functional behaviour compliance is the Ada engineering goal, assisted by the SPARK guidelines). > Therefore it becomes practicable to reason about the behaviour of a > SPARK program based solely on the analysis of the program text. Annotations are the static analysis directives to be established by Software Engineers to increase the software product likelihood to behave as intending, and reduce risks of error to an acceptable level. > > I means since SPARK is restricted to the best of Ada, is SPARK better > > than Ada to resolving complex engineering applications, or SPARK a > > better choice than C/C++ to address leaner systems? (in terms of > > compliance to early drafts of DO-178C - certification levels C to A). > > > Indeed, the successful applications of SPARK bring to results that are > > rather difficult to compare. > > > “The formal design of Tokeneer ID Station (TIS) shows the TIS system > > to be a purely sequential system.” - (INFORMED design, at section > > 2.2, Identification of the SPARK boundary) > > Support for concurrent programs (RavenSPARK) was added in 2003. (Tokeneer was also on how to accede the administrator and user ID station simultaneously). Rather, “Purely sequential system” doesn't refer to single task, but to the “sequential logic of a finite state machine”. That is what Tokeneer is, and what the INFORMED design means. Therefore, Tokeneer was fairly straight forward to prove, just a little was done and everything worked! > > “We believe part of the success of proof on SHOLIS is due to the > > simple system architecture. … > > Some large-scale SPARK reasoning are also needed, including support > > for abstract proof, before the technology can be extensively used at > > the highest level of large systems.” - (Is Proof More Cost Effective > > Than Testing – Section 8, Summary). > > Support for abstract proof was added in 2000. > > > > > Beyond any theory or academic project, 10 years later, from all the > > past SPARK projects’ experiences, does it happen that SPARK can > > address “purely sequential systems” or that SPARK “can be extensively > > used at the highest level of large systems”? > > An example of a large, concurrent SPARK program is iFACTS - described > by the UK National Air Traffic Service as "the biggest change in air > traffic control since radar". Feb 2010, the ERCIM Working Group on Formal Methods for Industrial Critical Systems stated: “There is a lack of precedents where formal methods have been proven to be effective.” http://www.inrialpes.fr/vasy/fmics/ Did the ECRIM overlook iFACTS? Formal Methods (i.e., Z notation and SPARK) are best suited to the development of data oriented, sequential systems. i.e., they are generally sufficient to demonstrate data flow correctness and SPARK can prove the absence of run time error. But on how to handle the functional complexities of large systems, they had always led to dead ends, almost. > > Claude > > Cheers, > > Phil iFACTS: What has been accomplished there? Does the abstract proofs were able to consider and address all functional validations? Were traditional testing involved and did they do all the functional verification: (over data flow correctness and proof of absence of run time error)? ------------------------------------------------------ There are boundaries there, which need to be clarified. ------------------------------------------------------ Thanks Phil Claude ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-12 18:09 ` Claude @ 2010-06-12 19:27 ` Yannick Duchêne (Hibou57) 2010-06-17 5:38 ` Claude 2010-06-13 5:37 ` J-P. Rosen 1 sibling, 1 reply; 12+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-06-12 19:27 UTC (permalink / raw) Le Sat, 12 Jun 2010 20:09:48 +0200, Claude <claude.defour@orange.fr> a écrit: > Formal Methods (i.e., Z notation and SPARK) are best suited to the > development of data oriented, sequential systems. i.e., they are > generally sufficient to demonstrate data flow correctness and SPARK > can prove the absence of run time error. But on how to handle the > functional complexities of large systems, they had always led to dead > ends, almost. Sure there is way to... (it must be) Sorry for being a bit out of topic, I would like to ask you a question, as it seems you know about the sate of the art. Please, do you know if there are accessible documents about balancing intuitionistic logic vs classical logic in this area ? -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-12 19:27 ` Yannick Duchêne (Hibou57) @ 2010-06-17 5:38 ` Claude 0 siblings, 0 replies; 12+ messages in thread From: Claude @ 2010-06-17 5:38 UTC (permalink / raw) On Jun 12, 12:27 pm, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr> wrote: > Le Sat, 12 Jun 2010 20:09:48 +0200, Claude <claude.def...@orange.fr> a > écrit:> Formal Methods (i.e., Z notation and SPARK) are best suited to the > > development of data oriented, sequential systems. i.e., they are > > generally sufficient to demonstrate data flow correctness and SPARK > > can prove the absence of run time error. But on how to handle the > > functional complexities of large systems, they had always led to dead > > ends, almost. > > Sure there is way to... (it must be) Once Peter Amey (prime author of SPARK Examiner) stated: "what can be achieved is limited by precision of descriptions and notations used". "What we can achieve depends on the properties of the language we are analysing". (ref: IEC 61508-conformant software development with SPARK) The language is Ada. With that there is a long list of successfully implemented large complex safety critical systems. The SPARK tools are Prolog applications. With that there is a lot of expert systems, and theorem proving applications. Formal methods have been advocated as a means of increasing the reliability of systems. Puting it together, what can we do? Data flow control and code properties verification... Therefore, how Formal Methods can address the functional aspect of the system behaviour? --------- The behaviour of reactive systems is largely conditioned by the interaction with events of the external environment the sequentialization of which is not predictable. The complexity of the systems' behaviour increases considerably when the timing dependencies in the execution of events are taken into account. The above features are typical of a large class of systems including control systems, automation systems, and communication systems and results in the extreme difficulty of the verification of their correctness. http://www.inrialpes.fr/vasy/fmics/ --------- How Formal Methods can assess unpredictable sequentialization, dependencies, complexity, and achieves that "extreme difficulty of the verification of correctness."? Phil Thornley, said that iFACTS could be part of the answer. But, on what SPARK is about, the uncertainty stays still... Does the abstract proofs were able to consider and address all functional validations? Were traditional testing involved and did they do all the functional verification: (over data flow correctness and proof of absence of run time error)? ------------------------------------------------------ There are boundaries there, which need to be clarified. ------------------------------------------------------ > > Sorry for being a bit out of topic, I would like to ask you a question, as > it seems you know about the state of the art. Please, do you know if there > are accessible documents about balancing intuitionistic logic vs classical > logic in this area ? > My knowledge is mostly founded on experiences. But I know that Peter Amey was relating to "Bayesian mathematics" as the limits what could be claimed from statistical testing. "Bayesian probability interprets the concept of probability as "a measure of a state of knowledge", in contrast to interpreting it as a frequency or a physical property of a system." Claude Defour ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-12 18:09 ` Claude 2010-06-12 19:27 ` Yannick Duchêne (Hibou57) @ 2010-06-13 5:37 ` J-P. Rosen 2010-06-13 8:11 ` Simon Wright ` (2 more replies) 1 sibling, 3 replies; 12+ messages in thread From: J-P. Rosen @ 2010-06-13 5:37 UTC (permalink / raw) Claude a �crit : > Feb 2010, the ERCIM Working Group on Formal Methods for Industrial > Critical Systems stated: �There is a lack of precedents where formal > methods have been proven to be effective.� > http://www.inrialpes.fr/vasy/fmics/ > > Did the ECRIM overlook iFACTS? > More surprisingly, did they overlook Meteor (100% automated line 14 of the Parisian subway, in B+Ada) ? -- --------------------------------------------------------- J-P. Rosen (rosen@adalog.fr) Visit Adalog's web site at http://www.adalog.fr ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-13 5:37 ` J-P. Rosen @ 2010-06-13 8:11 ` Simon Wright 2010-06-13 13:20 ` Robert A Duff 2010-06-17 2:10 ` Claude 2 siblings, 0 replies; 12+ messages in thread From: Simon Wright @ 2010-06-13 8:11 UTC (permalink / raw) "J-P. Rosen" <rosen@adalog.fr> writes: > Claude a écrit : >> Feb 2010, the ERCIM Working Group on Formal Methods for Industrial >> Critical Systems stated: “There is a lack of precedents where formal >> methods have been proven to be effective.” >> http://www.inrialpes.fr/vasy/fmics/ >> >> Did the ECRIM overlook iFACTS? >> > More surprisingly, did they overlook Meteor (100% automated line 14 of > the Parisian subway, in B+Ada) ? This is very relevant -- took a little googling (meteor paris metro ada formal b): http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-13 5:37 ` J-P. Rosen 2010-06-13 8:11 ` Simon Wright @ 2010-06-13 13:20 ` Robert A Duff 2010-06-17 2:10 ` Claude 2 siblings, 0 replies; 12+ messages in thread From: Robert A Duff @ 2010-06-13 13:20 UTC (permalink / raw) "J-P. Rosen" <rosen@adalog.fr> writes: > More surprisingly, did they overlook Meteor (100% automated line 14 of > the Parisian subway, in B+Ada) ? And nobody wants to see an error message, "Constraint_Error on line 14". ;-) - Bob ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: What is SPARK about? 2010-06-13 5:37 ` J-P. Rosen 2010-06-13 8:11 ` Simon Wright 2010-06-13 13:20 ` Robert A Duff @ 2010-06-17 2:10 ` Claude 2 siblings, 0 replies; 12+ messages in thread From: Claude @ 2010-06-17 2:10 UTC (permalink / raw) On Jun 12, 10:37 pm, "J-P. Rosen" <ro...@adalog.fr> wrote: > Claude a crit :> Feb 2010, the ERCIM Working Group on Formal Methods for Industrial > > Critical Systems stated: There is a lack of precedents where formal > > methods have been proven to be effective. > >http://www.inrialpes.fr/vasy/fmics/ > > > Did the ECRIM overlook iFACTS? > > More surprisingly, did they overlook Meteor (100% automated line 14 of > the Parisian subway, in B+Ada) ? > > -- > --------------------------------------------------------- > J-P. Rosen (ro...@adalog.fr) > Visit Adalog's web site athttp://www.adalog.fr Hello Jean-Pierre, ------------ http://www.bmethod.com/pdf/grace-2010/1-the-big-picture.pdf ------------ B into industrial existence (page 5): - turned out to be a real success: - 86 k loc software - still in v1.0 today, no bug detected so far B for systems: the reasons (page 8) - 100% proved software is not a guaranty per se - Even if METEOR ATP is still in v1.0 in 2010 - Ex: ATP reverse-engineered, from existing wired-logic systems to Programmable Logic Controller (PLC) - Not able to stop precisely at station - Software 100% proved but its specification was not the one that could make the train stopping ------------ 86 k loc to supersede wired-logic (e.g., Metro line D). That kind of Railway automated systems is about sequential logic and finite state machine. Therefore, that is right within the scope of formal methods. (A+) i.e., Since the specifications of the whole system (formerly wired- logic) could be expressed as a set of provable statements, automated tools were able to explicitly address the functional aspects of the specified behaviour. That might explain why the ERCIM Working Group on Formal Methods for Industrial Critical Systems was "Not able to stop precisely at the METEOR station" Next Station ... iFACTS?!??? Claude ^ permalink raw reply [flat|nested] 12+ messages in thread
end of thread, other threads:[~2010-06-17 5:38 UTC | newest] Thread overview: 12+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2010-06-11 20:32 What is SPARK about? Claude 2010-06-11 23:01 ` Simon Wright 2010-06-11 23:17 ` Yannick Duchêne (Hibou57) 2010-06-12 12:16 ` Peter C. Chapin 2010-06-12 8:30 ` Phil Thornley 2010-06-12 18:09 ` Claude 2010-06-12 19:27 ` Yannick Duchêne (Hibou57) 2010-06-17 5:38 ` Claude 2010-06-13 5:37 ` J-P. Rosen 2010-06-13 8:11 ` Simon Wright 2010-06-13 13:20 ` Robert A Duff 2010-06-17 2:10 ` Claude
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox