From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,b03962e55f213a92 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!34g2000prs.googlegroups.com!not-for-mail From: Claude Newsgroups: comp.lang.ada Subject: Re: What is SPARK about? Date: Wed, 16 Jun 2010 22:38:59 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 70.79.53.248 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1276753140 29510 127.0.0.1 (17 Jun 2010 05:39:00 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 17 Jun 2010 05:39:00 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: 34g2000prs.googlegroups.com; posting-host=70.79.53.248; posting-account=WPcl4AoAAAC3CTqLAgWnftzSSCqiCJ4J User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.3) Gecko/20100401 Firefox/3.6.3,gzip(gfe) Xref: g2news2.google.com comp.lang.ada:12765 Date: 2010-06-16T22:38:59-07:00 List-Id: On Jun 12, 12:27=A0pm, Yannick Duch=EAne (Hibou57) wrote: > Le Sat, 12 Jun 2010 20:09:48 +0200, Claude a = =A0 > =E9crit:> 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. =A0But 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, a= s =A0 > it seems you know about the state of the art. Please, do you know if ther= e =A0 > are accessible documents about balancing intuitionistic logic vs classica= l =A0 > 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