RE: [SysML Forum] SysML and verification
edi...@sysmlforum.com
> I see in the SysML documentation "verification" mentioned some times, but
> have not been able to grasp what this imeans in that context. Is is "formal verification"?
No, the term "verification" in the context of SysML refers to
"Requirements verification" (as in Requirements "Verification &
Validation" or "V&V") rather than the "formal verification" associated
with formal methods related to mathematics.
SysML support for Requirements V&V is explained more fully in the
following FAQ, which also includes an example:
SysML FAQ: How does SysML enable Requirements Verification and
Validation (V&V)?
http://www.sysmlforum.com/faq/how-does-sysml-enable-requirements-verification-and-validation.html
- OR -
http://tinyurl.com/lt6szec
Best,
Cris
__________________________________________________
Cris Kobryn
Editor, SysML Forum
mailto:edi...@SysMLforum.com
www.SysMLforum.com
> -------- Original Message --------
> Subject: [SysML Forum] SysML and verification
> From: Øyvind_Teig <oyvin...@gmail.com>
> Date: Fri, June 07, 2013 2:19 am
> To: sysml...@googlegroups.com
>
>
> I see in the SysML documentation "verification" mentioned some times, but
> have not been able to grasp what this imeans in that context,
>
> Is is "formal verification"? Examples of formal verification would, as far
> as I understand it be:
>
> - CSPm language and FDR2 tool
> - Promela language and Spin tool
> - CSP-type language and PAT tool (Process Analysis Toolkit)
>
> Pasting from http://en.wikipedia.org/wiki/PAT_(model_checker) then PAT
> would analyse and formally verify "properties such as deadlock-freeness,
> divergence-freeness, reachability, LTL properties with fairness
> assumptions, refinement checking and probabilistic model checking".
>
> 1. Is the SysML *verification* along this path?
> 2. Which diagram type(s) will in case be verified?
> 3. How is modeling errors reported to the user?
> 4. Would Rhapsody with SysML be able to do any of this?
>
> Øyvind Teig
> Trondheim Norway
>
> --
> --
> You received this message because you are subscribed to the Google
> Groups "SysML Forum" group.
> Public website: http://www.SysMLforum.com
> To post to this group, send email to sysml...@googlegroups.com
> To unsubscribe from this group, send email to
> sysmlforum+...@googlegroups.com
> For more options, visit this group at
> http://groups.google.com/group/sysmlforum?hl=en_US?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "SysML Forum" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sysmlforum+...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
edi...@sysmlforum.com
> Since "Requirement Validation" would mean "Am I building the right
> requirement?" (product == the requirement in itself) (a rather meaningless
> sentence, since the requirement itself is not the product,
Your simplistic substitution of "requirement" for "product" in Boehm's
informal definition of "Validation" sacrifices correctness for
conciseness, since it is inconsistent with the semantics of his
preceding formal definition ("... to establish the fitness or worth of a
software product ...").
If you want to apply Boehm's formal distinction between V&V more
specifically to Requirement specifications, an elaboration will serve
better than a simplistic substitution. Consider the following:
Requirements Validation: "Am I building the right product, which is
worthy of its operational mission as specified by its (testable)
requirements?"
> Same for verification.
Likewise, Requirements Verification can be elaborated as follows:
Requirements Verification: ""Am I building the product right, where
there is a straightforward mapping ("truthful correspondence") between
all requirements specifications and tests that demonstrate ("verify")
how those requirements are fulfilled ("satisfied") by the subject
product.
Both elaborations above are consistent with [Boehm 84] as well as the
discussion and example in the relevant SysML FAQ ("How does SysML enable
Requirements Verification V&V"; see http://tinyurl.com/lt6szec). While
both elaborations may be further condensed, here I emphasize correctness
over conciseness.
/ck
__________________________________________________
Cris Kobryn
Editor, SysML Forum
mailto:edi...@SysMLforum.com
www.SysMLforum.com
> -------- Original Message --------
> Subject: Re: [SysML Forum] SysML and verification
> From: Øyvind_Teig <oyvin...@gmail.com>
> Date: Mon, June 10, 2013 4:26 am
> To: sysml...@googlegroups.com
> Cc: edi...@SysMLforum.com
>
>
> Thanks, Cris
>
> Verification:"Am I building the product right?"
> Validation:"Am I building the right product?"
>
> Since "Requirement Validation" would mean "Am I building the right
> requirement?" (product == the requirement in itself) (a rather meaningless
> sentence, since the requirement itself is not the product, it needs to
> reach out for the product) why isn't it called "Validation of the product's
> requirement"? Is this just how the natural language is: not necesary
> logical?
>
> Same for verification.
>
> Øyvind Teig
>
> On Monday, June 10, 2013 9:58:19 AM UTC+2, edi...@SysMLforum.com wrote:
> >
> > Hej Øyvind,
> >
> > > I see in the SysML documentation "verification" mentioned some times,
> > but
> > > have not been able to grasp what this imeans in that context. Is is
> > "formal verification"?
> >
> > No, the term "verification" in the context of SysML refers to
> > "Requirements verification" (as in Requirements "Verification &
> > Validation" or "V&V") rather than the "formal verification" associated
> > with formal methods related to mathematics.
> >
> > SysML support for Requirements V&V is explained more fully in the
> > following FAQ, which also includes an example:
> >
> > SysML FAQ: How does SysML enable Requirements Verification and
> > Validation (V&V)?
> >
> > http://www.sysmlforum.com/faq/how-does-sysml-enable-requirements-verification-and-validation.html
> > - OR -
> > http://tinyurl.com/lt6szec
> >
> > Best,
> >
> > Cris
> >
> > __________________________________________________
> > Cris Kobryn
> > Editor, SysML Forum
> > mailto:edi...@SysMLforum.com <javascript:>
> > > To post to this group, send email to sysml...@googlegroups.com<javascript:>
> > > To unsubscribe from this group, send email to
> > > sysmlforum+...@googlegroups.com <javascript:>
> > > For more options, visit this group at
> > > http://groups.google.com/group/sysmlforum?hl=en_US?hl=en
> > >
> > > ---
> > > You received this message because you are subscribed to the Google
> > Groups "SysML Forum" group.
> > > To unsubscribe from this group and stop receiving emails from it, send
> > an email to sysmlforum+...@googlegroups.com <javascript:>.
edi...@sysmlforum.com
> I thought that the mere susbtitution had a kind of flaw of the original term pop up,
> perhaps not noticed with natural language semantics.
I agree that natural language semantics are problematic, especially when
using historically kludgy languages such as English
(http://tinyurl.com/yeb4cxj). During the decade that I chaired and
edited the UML 1.x, UML 2.0, and Open Source SysML specification teams I
found fewer than a handful of contributors who could write what we
referred to as "precise English."
> I assume that you will not have this refinement relation in SysML?
No, there is already a <<refine>> relationship in SysML and its parent
language, UML2, that could be used or adapted for your purpose. As a
starting point, note the use of the <<refine>> relationship to trace the
System Design <<view>> entities to the System Analysis <<view>> entities
in the SysML FAQ previously cited in this thread ("How does SysML enable
Requirements Verification V&V"; see http://tinyurl.com/lt6szec). Please
let me know if you want to further discuss how <<refine>> could be
adapted for "formal verification" purposes (cf. "Requirements
verification") as per your example.
/ck
__________________________________________________
Cris Kobryn
Editor, SysML Forum
mailto:edi...@SysMLforum.com
www.SysMLforum.com
> -------- Original Message --------
> Subject: Re: [SysML Forum] SysML and verification
> From: Øyvind_Teig <oyvin...@gmail.com>
> Date: Tue, June 11, 2013 3:24 am
> To: sysml...@googlegroups.com
> Cc: edi...@SysMLforum.com
>
>
> Cris
>
> This sounds plausible! But I didn't mean to be only picky. I thought that
> the mere susbtitution had a kind of flaw of the original term pop up,
> perhaps not noticed with natural language semantics.
>
> In CSPm (tool is FDR2) and PAT an implementation is verified to be a
> "refined" (and more deterministic, since the spec doesn't care so much
> about detail) "version" of the specification. A system will not be modeled
> by a TestProgarm plus a ProgramUnderTest, but by a Specification and an
> Implementation, where Implementation refines Specification.
>
> I assume that you will not have this refinement relation in SysML?
>
> Øyvind Teig
> Trondheim
>
> kl. 04:37:01 UTC+2 tirsdag 11. juni 2013 skrev edi...@SysMLforum.com
> følgende:
Bernd GRAHLMANN
Dear all,,
Sorry to jump in a bit late …
In various industries and companies I have seen quite different ‘interpretations’/’definitions’ of the terms ‘validation’ and ‘verification’. I am not a fan of wasting plenty of time to fight over those ‘differences’. I rather propose to take a little step back and look at what is actually needed:
1. On the requirements end you have:
a. requirements from the user/customer in which the user/customer specifies what they require (note, that these requirements may actually be kind of independent of a specific system/sub-system/component – as a user may not care what kind of system/product/device you offer him/her to achieve something);
b. ‘technical’ requirements for the different scopes of the system decomposition (i.e., the system, each sub-system, each component, … – note that in case of high complexity ... different aspects may even be dealt with separately);
2. On the ‘qualification’ (to bring in a more general term) end you (may or may not – depending on your effort versus risk evaluation) have:
a. Qualification measure(s) for each user/customer requirement;
b. Qualification measure(s) for each technical requirement;
3. In addition, you have an interest to perform measures to check whether the various engineering steps have been performed successfully. This could cover things like reviews whether derived sub-system requirements satisfy system requirements; or some standard (incl. syntax) checks of models, … Note, that this actually allows you to figure out problems earlier.
Note, that sometimes you may decide to have some qualification measure(s) performed on a model of the system/sub-system/component rather than the real one.
So, in essence, I do not really care ‘how you name it’, but you should come up with the above ;-)
Hope that helps + Thanks,
Bernd
Dr. Bernd GRAHLMANN
Requirements Engineering / Management / Development & DOORS
Expert / Trainer / Consultant
Tel.: +41 79 2967651
Fax.: +41 86 079 2967651
e-mail Be...@Grahlmann.net
From: sysml...@googlegroups.com [mailto:sysml...@googlegroups.com] On Behalf Of Stéphane Vayssier
Sent: Tuesday, June 11, 2013 10:06 PM
To: sysml...@googlegroups.com
Cc: edi...@SysMLforum.com
Subject: Re: [SysML Forum] SysML and verification
Hi Øyvind
The SysML Profile that is implemented in Artisan Studio provides some consistency checks that allows you to check the consistency of your model regarding SysML standard. It also provides an add-on to define some rules that will be checked in your model (some SysML rules are implemented by default, and you can define your own rules).
Defining rules that needs to be checked covers the "Verification" you are expecting. Some rules may be something like unused events, non-allocated activities ...
My point of view regarding system validation is mainly about system level simulation. Artisan Studio provides some tools to generate a simulation environment for simulating the system you build (and allowing some external simulation tools to interact with your system such as Simulink for more advanced behavior definition ...).
So, to sum up, for me
Verification = "Am I building the system right ? " = check consistency regarding SysML rules, your own design rules, and the consistency of the model
Validation = "Am I building the right system ? " = simulation to check the behavior you specified in your SysML model is the expected behavior.
Stephane
On Monday, June 10, 2013 1:26:01 PM UTC+2, Øyvind Teig wrote:
Thanks, Cris
Verification:"Am I building the product right?"
Validation:"Am I building the right product?"
Since "Requirement Validation" would mean "Am I building the right requirement?" (product == the requirement in itself) (a rather meaningless sentence, since the requirement itself is not the product, it needs to reach out for the product) why isn't it called "Validation of the product's requirement"? Is this just how the natural language is: not necesary logical?
Same for verification.
Øyvind Teig
On Monday, June 10, 2013 9:58:19 AM UTC+2, edi...@SysMLforum.com wrote:
Miller, Greg A (SGNCOE)
This may be a different perspective.
I was taught that an SE should reference industry standards whenever possible to have consistent definitions.
From the INCOSE Systems Engineer Handbook, v3.2.2:
From SAE ARP4754A:
From RTCA DO-178C:
From RTCA DO-254:
All four essential say:
Validation is the processes of determining that the correct requirement(s) (system, software, or hardware) have been specified for an intended use.
Verification is the processes of determining that the requirement(s) (system, software, or hardware) has (have) been met by the system, software, or hardware implementation.
There are a number of methods that may be used for validation and verification.
For Validation:
Traceability
Analysis
Modeling
Test
Similarity
Engineering Review
For Verification:
Inspection or Review
Analysis
Modeling
Coverage Analysis
Test or Demonstration
Greg Miller
Senior Systems Engineer
Aerospace - Minneapolis
Sensing, Guidance & Navigation COE
MN17-1622
2600 Ridgway Parkway
Minneapolis, MN 55413
(612) 951-5638 Voice
(612) 951-5069 FAX
greg.a...@honeywell.com