survey of industrial use of formal methods

[Daniel Jackson-6]

Dear Alloy Users,

Peter Gorm Larsen, Juan Bicarregui and John Fitzgerald are conducting  
a survey of industrial use of formal methods and plan to issue an  
initial report at FM'08 this summer.

If you are using Alloy in an industrial application, would you be  
willing to do the survey?

You can access it at:

        http://www.jiscmail.ac.uk/cgi-bin/surveys.cgi?A=hp&LMGT1=FMSURVEY

I'd be grateful if you'd let me know if you're using Alloy on an  
industrial project so I can help them collect data, even if you don't  
have time to complete the survey.

Regards,

--Daniel

[Rodney D Price]

Some parts of this message have been removed. Learn more about Nabble's security policy.

I'd be glad to do the survey (we are using Alloy in an industrial setting), but it seems that they want me to register my email, etc first.  Is this necessary?

-Rod

[e-mail] wrote: -----

To: [e-mail]
From: Daniel Jackson <dnj@....edu>
Sent by: [e-mail]
Date: 04/08/2008 04:40PM
Subject: [alloy-discuss] survey of industrial use of formal methods

Dear Alloy Users,

Peter Gorm Larsen, Juan Bicarregui and John Fitzgerald are conducting  
a survey of industrial use of formal methods and plan to issue an  
initial report at FM'08 this summer.

If you are using Alloy in an industrial application, would you be  
willing to do the survey?

You can access it at:

     http://www.jiscmail.ac.uk/cgi-bin/surveys.cgi?A=hp&LMGT1=FMSURVEY

I'd be grateful if you'd let me know if you're using Alloy on an  
industrial project so I can help them collect data, even if you don't  
have time to complete the survey.

Regards,

--Daniel


------------------------------------

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/alloy-discuss/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/alloy-discuss/join
    (Yahoo! ID required)

<*> To change settings via email:
    alloy-discuss-digest@... 
    alloy-discuss-fullfeatured@...

<*> To unsubscribe from this group, send an email to:
    [e-mail]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/

__._,_.___

Messages in this topic (2) Reply (via web post) | Start a new topic

Messages | Files | Photos | Links | Database | Polls | Members | Calendar

Change settings via the Web (Yahoo! ID required)
Change settings via email: alloy-discuss-digest@... | alloy-discuss-traditional@...
Visit Your Group | Yahoo! Groups Terms of Use | alloy-discuss-unsubscribe@...

Recent Activity

•  4
  New Members

Visit Your Group

Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

Ads on Yahoo!

Learn more now.

Reach customers

searching for you.

How-To Zone

on Yahoo! Groups

Discuss home and

garden projects.

.

__,_._,___

[Daniel Jackson-6]

Rodney,

I don't know what the effect of the registration is.

Peter -- maybe you can tell us?

You can also complete the survey as a Word document (which I'm  
attaching) and email it to Peter.

--Daniel

On Apr 8, 2008, at 7:41 PM, Rodney D Price wrote:
> I'd be glad to do the survey (we are using Alloy in an industrial  
> setting), but it seems that they want me to register my email, etc  
> first.  Is this necessary?

 

[Daniel Jackson-6]

Thanks, Peter. I'm forwarding this to the list.

--Daniel

On Apr 9, 2008, at 10:37 AM, Peter Gorm Larsen wrote:

> Hi Daniel,
> At the on-line registration we ask for the email ONLY to be able to  
> get rid of any possible spam contributions. However, if you feel  
> more safe by sending the filled out word document by all means just  
> do that and send it to me. Thanks in advance for your contribution.
>
> Best wishes,
> Peter
>
> Peter Gorm Larsen
> Professor, PhD (ingeniørdocent)
> Engineering College of Aarhus
> Computer Technology & Embedded Systems
> Dalgas Avenue 2
> DK-8000 Aarhus C
> Denmark
> Phone [phone]
> Direct  [phone]
> Mobile [phone]
> Fax     [phone]
> URL    www.iha.dk

[Rodney D Price]

Some parts of this message have been removed. Learn more about Nabble's security policy.

A common way to solve the spam problem is the use of a captcha.  See http://www.captcha.net/captchas/

-Rod

[e-mail] wrote: -----

To: "Peter Gorm Larsen" <pgl@...>
From: Daniel Jackson <dnj@....edu>
Sent by: [e-mail]
Date: 04/09/2008 08:49AM
cc: [e-mail]
Subject: Re: [alloy-discuss] survey of industrial use of formal methods

Thanks, Peter. I'm forwarding this to the list.

--Daniel

On Apr 9, 2008, at 10:37 AM, Peter Gorm Larsen wrote:

> Hi Daniel,
> At the on-line registration we ask for the email ONLY to be able to  
> get rid of any possible spam contributions. However, if you feel  
> more safe by sending the filled out word document by all means just  
> do that and send it to me. Thanks in advance for your contribution.
>
> Best wishes,
> Peter
>
> Peter Gorm Larsen
> Professor, PhD (ingeniørdocent)
> Engineering College of Aarhus
> Computer Technology & Embedded Systems
> Dalgas Avenue 2
> DK-8000 Aarhus C
> Denmark
> Phone [phone]
> Direct  [phone]
> Mobile [phone]
> Fax     [phone]
> URL    www.iha.dk

------------------------------------

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/alloy-discuss/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/alloy-discuss/join
    (Yahoo! ID required)

<*> To change settings via email:
    alloy-discuss-digest@... 
    alloy-discuss-fullfeatured@...

<*> To unsubscribe from this group, send an email to:
    [e-mail]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/

__._,_.___

Messages in this topic (5) Reply (via web post) | Start a new topic

Messages | Files | Photos | Links | Database | Polls | Members | Calendar

Change settings via the Web (Yahoo! ID required)
Change settings via email: alloy-discuss-digest@... | alloy-discuss-traditional@...
Visit Your Group | Yahoo! Groups Terms of Use | alloy-discuss-unsubscribe@...

Recent Activity

•  4
  New Members

Visit Your Group

Yahoo! Finance

It's Now Personal

Guides, news,

advice & more.

New business?

Get new customers.

List your web site

in Yahoo! Search.

Featured Y! Groups

and category pages.

There is something

for everyone.

.

__,_._,___

[Irina Rychkova]

 Hello!

I wonder, how I can make a valid assertion about a data structure in alloy?
I tried the following example:

pred B [b: one Int, x:one Int]{
(b>0) => (x=b)
}
assert is_B{
all b: Int | some x : Int  | B[b,x]
}
This assertion, up to my understanding, means that for any b we can always find x such as if b>0 then x=b . This assertion is valid .

Now I make the similar assertion where x is the element  of X.
sig X{v: one Int}

pred A [b: one Int, x:one X]{
(b>0) => (x.v=b)
}
assert is_A{
all b: Int | some x:X | A[b,x]
}
However the counterexample is found. How can I deal with x in this case to make a valid assertion?
Best regards,
Irina

[Felix Chang-2]

On Thu, 10 Apr 2008, Rychkova Irina wrote:
> pred B [b: one Int, x:one Int] { (b>0) => (x=b) }
> assert { all b: Int | some x : Int  | B[b,x] }
>
> This assertion, up to my understanding,
> means that for any b we can always find x such as if b>0 then x=b.
> This assertion is valid.

Yes.  But this assertion is valid because Alloy4's semantics
ensures the existence of every integer between MIN and MAX.

> Now I make the similar assertion where x is the element of X.
>
> sig X {v: one Int}
> pred A [b: one Int, x:one X] { (b>0) => (x.v=b) }
> assert { all b: Int | some x:X | A[b,x] }
>
> However the counterexample is found.

That's because you didn't say that every X must map to a distinct integer
(and also, somewhat less importantly, in this particular case
you only have 3 X atoms and 7 positive integers,
so by the pigeon hole principle there must be some integer b
for which no X.v is equal to it)

This is the expected result of Alloy being a declarative language
and Alloy Analyzer being a model finder that tries its best to provide
you a counterexample:

if scope of X < scope of Int,
Alloy would just arbitrarily pick an integer b,
and then make sure none of the X atoms point to b.

if scope of X >= scope of Int,
Alloy would deliberately make sure two X happen to have the same v value,
and thus once again there exists some integer b
such that none of the X atom point to it.

Either way, your assertion has counterexamples.

>
> How can I deal with x in this case to make a valid assertion?
>

You can make this a "valid assertion" by forcing there to be exactly 16 X atoms,
and forcing them to all point to different integers.
That way, then indeed for every b:Int, there is some x:X, such that b=x.v.

sig X {v: one Int}
pred A [b: one Int, x:one X] { (b>0) => (x.v=b) }
fact { all disj a, b: X | a.v != b.v }
check { all b: Int | some x:X | A[b,x] } for exactly 16 X

Sincerely,
Felix Chang
Alloy4 Developer

[Irina Rychkova]

Hello Felix,
Thank you for your answer,

Then I'm still puzzled, if it is at all possible to reason about data structures using assertions with Alloy?
I write action specifications in the form
Action [state_before, state_after]{
Precondition(state_before) => postcondition(state_after)
}
Where states 'before' and 'after' are tuples of variables of some type (not only integers).
I would like to validate my action specifications by making an assertion that for all possible states before the action the action will have a state-after .

Can I do it using assertions?

Regards,
Irina


From: alloy-discuss@... [mailto:alloy-discuss@...] On Behalf Of Felix Chang
Sent: 10 April 2008 14:33
To: alloy-discuss@...
Subject: Re: [alloy-discuss] Assertions over data structures in Alloy


On Thu, 10 Apr 2008, Rychkova Irina wrote:
> pred B [b: one Int, x:one Int] { (b>0) => (x=b) }
> assert { all b: Int | some x : Int | B[b,x] }
>
> This assertion, up to my understanding,
> means that for any b we can always find x such as if b>0 then x=b.
> This assertion is valid.

Yes. But this assertion is valid because Alloy4's semantics
ensures the existence of every integer between MIN and MAX.

> Now I make the similar assertion where x is the element of X.
>
> sig X {v: one Int}
> pred A [b: one Int, x:one X] { (b>0) => (x.v=b) }
> assert { all b: Int | some x:X | A[b,x] }
>
> However the counterexample is found.

That's because you didn't say that every X must map to a distinct integer
(and also, somewhat less importantly, in this particular case
you only have 3 X atoms and 7 positive integers,
so by the pigeon hole principle there must be some integer b
for which no X.v is equal to it)

This is the expected result of Alloy being a declarative language
and Alloy Analyzer being a model finder that tries its best to provide
you a counterexample:

if scope of X < scope of Int,
Alloy would just arbitrarily pick an integer b,
and then make sure none of the X atoms point to b.

if scope of X >= scope of Int,
Alloy would deliberately make sure two X happen to have the same v value,
and thus once again there exists some integer b
such that none of the X atom point to it.

Either way, your assertion has counterexamples.

>
> How can I deal with x in this case to make a valid assertion?
>

You can make this a "valid assertion" by forcing there to be exactly 16 X atoms,
and forcing them to all point to different integers.
That way, then indeed for every b:Int, there is some x:X, such that b=x.v.

sig X {v: one Int}
pred A [b: one Int, x:one X] { (b>0) => (x.v=b) }
fact { all disj a, b: X | a.v != b.v }
check { all b: Int | some x:X | A[b,x] } for exactly 16 X

Sincerely,
Felix Chang
Alloy4 Developer

[Felix Chang-2]

On Thu, 10 Apr 2008, Rychkova Irina wrote:
> Then I'm still puzzled, if it is at all possible to reason
> about data structures using assertions with Alloy?

Certainly.  We would just have to be careful about what are
the preconditions, and what exactly we are checking.

> I write action specifications in the form
> Action [state_before, state_after] {
>   Precondition(state_before) => postcondition(state_after)
> }
> Where states 'before' and 'after' are tuples of
> variables of some type (not only integers).
> I would like to validate my action specifications
> by making an assertion that for all possible states
> before the action the action will have a state-after.

The way we would write the model really depends on what exactly
we are hoping to check.

You said for all possible prestate, you want there to be a post state.
Then you have to ensure that you give large enough scope such that
such a post state can exist.  (And sometimes this is not even possible,
since for some situation it would require an infinite number of states.)

For example, suppose I'm modeling linked lists.
And I want to say that for every list X and Y,
then the concatenation XY also exists.

Boom! The model can never succeed, since we would need an infinite
number of lists to satisfy the above formula.

So the question I would ask myself here is: what am I checking?

a) am I checking the correctness of a particular linked list implementation?
b) am I checking the general properties of all linked list?

In case (a), since Alloy Analyzer is a bounded checker, I would rephrase
the formula to say that for all lists X and Y, if concatenate(X,Y) succeeds,
then the result is a valid concatenation of X and Y. (And I can then
check this up to scope of 10 perhaps)

In case (b), let's say I'm checking the property that
there can never be a linked list where a node has two distinct successors.
This is a question about linked list in general, and is NOT tied
to a particular implementation.  In this case, I would not be asking
for the existence of a "post state" at all. Instead, I would once again
set a bound of perhaps 10, and then I can check, for all lists of
length up to 10, you will never see a list where one of the node has
two distinct successors.

For case (b), you would often want to use several "fact" paragraphs
to constrain the lists to all be well-formed, because you would
only care about the properties on well-formed linked list.

For case (a), however, you would generally NOT want to have "fact"
paragraphs for well-formness, because the well-formness is exactly
what we would be trying to check!  So putting it into a fact paragraph
would tell Alloy Analyzer to ignore all violations of them,
and thus every linked list implementation would "magically" seem correct.

In conclusion, it's not clear to me which type of property you're trying to
check; you would have to formulate your model, and your collection
of facts versus assertions accordingly.  And one of Alloy Analyzer's
main strengths is definitely the ability to prove complicated properties
over complicated data structures, up to a user-chosen scope.

Sincerely,
Felix Chang
Alloy4 Developer

[Irina Rychkova]

Thank you for such a detailed explanation.  Considering my specifications, I 'm checking the case (a) - the correctness of the particular spec. I.e. I'm interested in proving the  fact that the specification will never produce the erroneous post state starting from the correct pre-state.
Could you precise how would you specify a valid concatenation and then check it  if a concatenation has a signature concatenate(X,Y, Result)?

>In case (a), since Alloy Analyzer is a bounded checker, I would rephrase
>the formula to say that for all lists X and Y, if concatenate(X,Y) succeeds,
>then the result is a valid concatenation of X and Y. (And I can then
>check this up to scope of 10 perhaps)

Thank you!
Irina

From: alloy-discuss@... [mailto:alloy-discuss@...] On Behalf Of Felix Chang
Sent: 10 April 2008 17:09
To: alloy-discuss@...
Subject: RE: [alloy-discuss] Assertions over data structures in Alloy


On Thu, 10 Apr 2008, Rychkova Irina wrote:
> Then I'm still puzzled, if it is at all possible to reason
> about data structures using assertions with Alloy?

Certainly. We would just have to be careful about what are
the preconditions, and what exactly we are checking.

> I write action specifications in the form
> Action [state_before, state_after] {
> Precondition(state_before) => postcondition(state_after)
> }
> Where states 'before' and 'after' are tuples of
> variables of some type (not only integers).
> I would like to validate my action specifications
> by making an assertion that for all possible states
> before the action the action will have a state-after.

The way we would write the model really depends on what exactly
we are hoping to check.

You said for all possible prestate, you want there to be a post state.
Then you have to ensure that you give large enough scope such that
such a post state can exist. (And sometimes this is not even possible,
since for some situation it would require an infinite number of states.)

For example, suppose I'm modeling linked lists.
And I want to say that for every list X and Y,
then the concatenation XY also exists.

Boom! The model can never succeed, since we would need an infinite
number of lists to satisfy the above formula.

So the question I would ask myself here is: what am I checking?

a) am I checking the correctness of a particular linked list implementation?
b) am I checking the general properties of all linked list?

In case (a), since Alloy Analyzer is a bounded checker, I would rephrase
the formula to say that for all lists X and Y, if concatenate(X,Y) succeeds,
then the result is a valid concatenation of X and Y. (And I can then
check this up to scope of 10 perhaps)

In case (b), let's say I'm checking the property that
there can never be a linked list where a node has two distinct successors.
This is a question about linked list in general, and is NOT tied
to a particular implementation. In this case, I would not be asking
for the existence of a "post state" at all. Instead, I would once again
set a bound of perhaps 10, and then I can check, for all lists of
length up to 10, you will never see a list where one of the node has
two distinct successors.

For case (b), you would often want to use several "fact" paragraphs
to constrain the lists to all be well-formed, because you would
only care about the properties on well-formed linked list.

For case (a), however, you would generally NOT want to have "fact"
paragraphs for well-formness, because the well-formness is exactly
what we would be trying to check! So putting it into a fact paragraph
would tell Alloy Analyzer to ignore all violations of them,
and thus every linked list implementation would "magically" seem correct.

In conclusion, it's not clear to me which type of property you're trying to
check; you would have to formulate your model, and your collection
of facts versus assertions accordingly. And one of Alloy Analyzer's
main strengths is definitely the ability to prove complicated properties
over complicated data structures, up to a user-chosen scope.

Sincerely,
Felix Chang
Alloy4 Developer

[Felix Chang-2]

On Thu, 10 Apr 2008, Rychkova Irina wrote:
> Thank you for such a detailed explanation.
> Considering my specifications, I'm checking the case (a)
> - the correctness of the particular spec. I.e. I'm
> interested in proving the fact that the specification will
> never produce the erroneous post state starting from the
> correct pre-state. Could you precise
> how would you specify a valid concatenation and then check it if a
> concatenation has a signature concatenate(X,Y, Result)?

Here is a simple example of a linked list "prepend" operation
that people might write in a functional language:

// The set of possible values
sig Value { }

// Each node can have a "next" pointer
// Each node must have a "value"
sig Node { next: lone Node, value: Value }

// We use a "lone Node" to represent a list.
// That is, if the argument is empty, then that's an empty list.
// But if the argument is not empty, then it points to the first node.
// (The following predicate tests whether a given list is legal or not)
pred legal [n: lone Node] {
    // legal list must not contain cycles
    no x, y: n.*next | x in y.^next && y in x.^next
}

// This non-mutative predicate returns true
// if "post" is the result of prepending "v" onto "pre"
pred prepend [pre:lone Node, v:Value, post: lone Node] {
    post.value = v && post.next = pre
}

// This simple predicate returns true
// if the list contains the given value
pred contains [list:lone Node, v: Value] {
    v in list.*next.value
}

// First, let's make sure the model is not inconsistent.
// To do that, we ask Alloy to give us an interesting scenario
// where we have two nonempty lists a and b,
// and b is the result of prepending v onto a.
run {
    some a, b: lone Node |
    some v: Value |
    a.next!=none && b.next!=none && legal[a] && prepend[a, v, b]
}

// Second, let's check to see if the "prepend" operation
// does what we want it to do.
// To do that, we assert that for any 2 lists a and b,
// if a is well-formed to begin with, and b is the result of prepending v to a,
// then b must be well-formed, and that b will in fact contain v as a result.
check {
    all a, b: lone Node |
    all v: Value |
    (legal[a] && prepend[a, v, b]) => (legal[b] && contains[b, v])
}