Spin model checker is a validation and verification open source toolset to
verify algorithms for trace errors etc.
spinroot.com
Would you like to know more?
David
________________________________
From: Eric Decker <cire...@gmail.com>
To: David Blubaugh <davidblubaugh2...@yahoo.com>
Cc: "tinyos-help@millennium.berkeley.edu" <tinyos-help@millennium.berkeley.edu>
Sent: Wednesday, August 28, 2013 8:37 PM
Subject: Re: [Tinyos-help] SPIN MODEL CHECKER
what is a spin model checker? reference?
On Wed, Aug 28, 2013 at 12:11 PM, David Blubaugh <davidblubaugh2...@yahoo.com>
wrote:
Has anyone ever used the spin model checker for verifying and validating
designs within TinyOS???
>
>Also, can the designs with tinyos be of any large complexity or is there a
>limit to the complexity of design???
how do you define complexity? how do you measure it?
tinyos programs are typically limited by RAM and code size.
>David Blubaugh
>
>
>
>
>
>
>
>
>
>From: "tinyos-help-requ...@millennium.berkeley.edu"
><tinyos-help-requ...@millennium.berkeley.edu>
>To: tinyos-help@millennium.berkeley.edu
>Sent: Wednesday, August 28, 2013 3:00 PM
>Subject: Tinyos-help Digest, Vol 124, Issue 26
>
>
>Send Tinyos-help mailing list submissions to
> tinyos-help@millennium.berkeley.edu
>
>To subscribe or unsubscribe via the World Wide Web, visit
> https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help
>
>or, via email, send a message with subject or body 'help' to
> tinyos-help-requ...@millennium.berkeley.edu
>
>You can reach the person managing the list at
> tinyos-help-ow...@millennium.berkeley.edu
>
>When replying, please edit your Subject line so it is more specific
>than "Re: Contents of Tinyos-help digest..."
>
>
>Today's Topics:
>
> 1. LEAP+ Protocol (Syed Abdul basir)
> 2. Help:Telosb BaseStation (Nilavra Pathak)
>
>
>----------------------------------------------------------------------
>
>Message: 1
>Date: Wed, 28 Aug 2013 04:19:20 -0700 (PDT)
>From: Syed Abdul basir <basir...@yahoo.com>
>Subject: [Tinyos-help] LEAP+ Protocol
>To: "tinyos-help@millennium.berkeley.edu"
> <tinyos-help@millennium.berkeley.edu>
>Message-ID:
> <1377688760.98794.yahoomail...@web162405.mail.bf1.yahoo.com>
>Content-Type: text/plain; charset="iso-8859-1"
>
>I am trying to compile leap+ code. getting the following error. can any one
>help me thanks.? the red highlightederrors. thanks.
>
>
>
>In file included from myLeapAppC.nc:17:
>In component `myLeapP':
>myLeapP.nc:31: interface MYA not found
>In file included from myLeapAppC.nc:17:
>myLeapP.nc:55: syntax error before `uint32_t'
>myLeapP: `ReceiveHello.receive' not implemented
>myLeapP: `TimerLed1Toggle.fired' not implemented
>myLeapP: `AMControl.startDone' not implemented
>myLeapP: `AMControl.stopDone' not implemented
>myLeapP: `TimerTimeStamp.fired' not implemented
>myLeapP: `Boot.booted' not implemented
>myLeapP: `AMSendTimeStamp.sendDone' not implemented
>myLeapP: `TimerHello.fired' not implemented
>myLeapP: `ReceiveStart.receive' not implemented
>myLeapP: `TimerMsgs.fired' not implemented
>myLeapP: `AMSendAck.sendDone' not implemented
>myLeapP: `TimerMain.fired' not implemented
>myLeapP: `TimerACK.fired' not implemented
>myLeapP: `AMSendTimeKeys.sendDone' not implemented
>myLeapP: `TimerHelloCount.fired' not implemented
>myLeapP: `TimerLed2Toggle.fired' not implemented
>myLeapP: `AMSendHello.sendDone' not implemented
>myLeapP: `TimeTimeKeys.fired' not implemented
>myLeapP: `ReceiveAck.receive' not implemented
>myLeapP: `TimerLed0Toggle.fired' not implemented
>In file included from
>/opt/tinyos-2.1.0/tos/chips/cc2420/packet/sim/CC2420PacketC.nc:25,
>???????????????? from
>/opt/tinyos-2.1.0/tos/chips/cc2420/csma/sim/CC2420CsmaC.nc:16,
>???????????????? from
>/opt/tinyos-2.1.0/tos/chips/cc2420/sim/CC2420RadioC.nc:63,
>???????????????? from
>/opt/tinyos-2.1.0/tos/chips/cc2420/sim/CC2420ActiveMessageC.nc:75,
>???????????????? from
>/opt/tinyos-2.1.0/tos/platforms/micaz/sim/ActiveMessageC.nc:61,
>???????????????? from myLeapAppC.nc:18:
>In component `CC2420PacketP':
>/opt/tinyos-2.1.0/tos/chips/cc2420/packet/sim/CC2420PacketP.nc: In function
>`getNetwork':
>/opt/tinyos-2.1.0/tos/chips/cc2420/packet/sim/CC2420PacketP.nc:66: warning:
>initialization from incompatible pointer type
>/opt/tinyos-2.1.0/tos/chips/cc2420/lpl/DummyLplC.nc:39:2: warning: #warning
>"*** LOW POWER COMMUNICATIONS DISABLED ***"
>make: *** [sim-exe] Error 1
>-------------- next part --------------
>An HTML attachment was scrubbed...
>URL:
>https://www.millennium.berkeley.edu/pipermail/tinyos-help/attachments/20130828/fdb9aaad/attachment-0001.htm
>
>------------------------------
>
>Message: 2
>Date: Wed, 28 Aug 2013 09:04:38 -0400
>From: Nilavra Pathak <nilav...@umbc.edu>
>Subject: [Tinyos-help] Help:Telosb BaseStation
>To: tinyos-help@millennium.berkeley.edu,
> tinyos-help-requ...@millenniym.berkeley.edu
>Message-ID:
> <CADfuJwKQtSSK==h2a_dFkRwHbpTAmaPpH7=5pwujihyvo30...@mail.gmail.com>
>Content-Type: text/plain; charset="iso-8859-1"
>
>Hey Guys,
>
>I have tried to make the BaseStation program run in the Telosb mote. I am
>using Ubuntu 13.04 for this .
>
>But every-time I try running the program nothing happens.
>
>To test whether the mote is working or not I have run the Blink program and
>it worked perfectly well .
>
>So help please.
>
>-Nilavra.
>-------------- next part --------------
>An HTML attachment was scrubbed...
>URL:
>https://www.millennium.berkeley.edu/pipermail/tinyos-help/attachments/20130828/c3c09c20/attachment-0001.htm
>
>------------------------------
>
>_______________________________________________
>Tinyos-help mailing list
>Tinyos-help@millennium.berkeley.edu
>https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help
>
>End of Tinyos-help Digest, Vol 124, Issue 26
>********************************************
>
>
>
>_______________________________________________
>Tinyos-help mailing list
>Tinyos-help@millennium.berkeley.edu
>https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help
>
--
Eric B. Decker
Senior (over 50 :-) Researcher
_______________________________________________
Tinyos-help mailing list
Tinyos-help@millennium.berkeley.edu
https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help
