The full Effective Model-Based Testing with Spec Explorer Class is now available!

Question

The full video series for the modeling class is available on Channel 9! It’s the recording of a two-half-day course Wolfgang and I gave at Microsoft's Redmond campus.

The training is long (about 8 hours), but we have split it for your viewing convenience into 4 lectures (sessions). Each session has in turn 4 parts.

Session 1

Session 2

Session 3

Session 4

Enjoy!

Caveat: The quality of the screen captures makes them hard to read. These videos will be replaced with new ones recorded with a better quality in the future. Please, forgive any inconvenience this might cause you.

Answer 1

Hi Nico,

would it be possible that we get the codes of the samples? For instance, the Stop Watch sample is really interesting for me.

Answer 2

Hi Bob,

The samples of lectures 1, 3 and 4 are already distributed as samples with Spec Explorer. The entire code of Stop Watch sample is in the slides. Here it is.

-------------------------------------------------------Model.cs

using System;
using System.Collections.Generic;
using System.Text;

using Microsoft.Modeling;

namespace StopwatchModel
{
    static class Model
    {
        public enum TimerMode { Reset, Running, Stopped }
      
        static bool displayTimer = false;
        static TimerMode timerMode = TimerMode.Reset;
        static bool timerFrozen = false;

        [Rule] static void ModeButton()
        {
            displayTimer = !displayTimer;
        }

        [Rule] static void StartStopButton()
        {
            Condition.IsTrue(displayTimer);
            if (timerMode == TimerMode.Running)
            {
                timerMode = TimerMode.Stopped;
                timerFrozen = false;
            }
            else
                timerMode = TimerMode.Running;
        }

        [Rule] static void ResetLapButton()
        {
            Condition.IsTrue(displayTimer);
            Condition.IsFalse(timerMode == TimerMode.Reset);
            if (timerMode == TimerMode.Running)
                timerFrozen = !timerFrozen;
            else
                timerMode = TimerMode.Reset;
        }              

        [Rule] static bool IsTimerReset()
        {
            return timerMode == TimerMode.Reset;
        }

        [Probe]
        public static string DisplayState()
        {
            return String.Format("{0}|{1}{2}",
                displayTimer ? "Timer" : "DateTime",
                timerMode,
                timerFrozen ? "|Frozen" : "");
        }

                            
    }
}

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

-------------------------------------------------------Config.cord

config Config
{
 action abstract static void Stopwatch.ModeButton();
 action abstract static void Stopwatch.StartStopButton();
 action abstract static void Stopwatch.ResetLapButton();

  action abstract static bool Stopwatch.IsTimerReset();

 action abstract static void Stopwatch.Initialize();

    switch generatedtestpath = "..\\TestSuite";
    switch testclassbase = "vs";
    switch StateBound = 512;
    switch StepBound = 512;
    switch PathDepthBound = 512;
    switch TestEnabled = false;
    switch RecommendedViews = "StateDescriptions";
}

machine Model() : Config
{
 construct model program from Config
  where namespace = "StopwatchModel"
 
}

machine TestSuite() : Config where TestEnabled = true
{
 construct test cases
  where strategy = "shorttests"
 for (Initialize; Model)
}

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

Answer 3

But what about the code of the Stopwatch under test?  Is that a downloadable sample?   -sulu

Answer 4

Nope. That's left as an excercise to the students :).

Answer 5

Hi Nico!

I'm having trouble downloading ANY of the class videos (any file-type).  I've tried several different downloaders (e.g., FDM, JDownloader) as well as simple IE "Open" and "Save As" actions.  The links all appear dead.

Could you please check to ensure the class videos are still online?  (If they aren't and you have to reupload them, could you please at least reupload the 2MB HD versions?  The lower resolution versions are probably difficult to read the slides...)  ((Also, are the slides available for download?  If they are, then I could tolerate the lower resolution versions...))

Thanks! -- Steve

P.S. - For point of reference, I'm in Silicon Valley and connected through Comcast broadband.  I've also tried MSN Dial-Up (my backup) and the same issue occurs...

 

Answer 6

Hi Steve,

Thanks for reporting this! I just checked with the Channel 9 team. They were able to track this back to a hardware problem with one of the servers. They are currently working to fix the problem. I'll let you know here as soon as I hear back from them.

Best,

Nico

Answer 7

I'm told the problem has been solved. Please try again and let me know if you find any issues.

My apologies for the inconvenience.

Nico

Answer 8

Hi Nico,

My name is Ignacio Cuevas and I am working as a test engineer for automotive applications in LEAR Coorp. The System testing group of my company will be very interesting to use Spec Explorer for testing software embbeded applications in our Electronic Control Units. Could be possible for you to make us a short seminar by web just to have an introduction for the tool. I wacth all videos and I found them really interesting but we will be around 20 people attending to that seminar and just with 1 h of your time will be enough to show to everyone include my manager the advantatges your tool can give us. Please, contact with me in my professional mail: [e-mail]. And we can discuss more of it. Thanks a lot!!

Best regards,

Answer 9

Hi Nico,

My name is Ignacio Cuevas and I am working as a test engineer for automotive applications in LEAR Coorp. The System testing group of my company will be very interesting to use Spec Explorer for testing software embbeded applications in our Electronic Control Units. Could be possible for you to make us a short seminar by web just to have an introduction for the tool. I wacth all videos and I found them really interesting but we will be around 20 people attending to that seminar and just with 1 h of your time will be enough to show to everyone include my manager the advantatges your tool can give us. Please, contact with me in my professional mail: [e-mail]. And we can discuss more of it. Thanks a lot!!

Best regards,

Hi Ignacio,

I've been trying to reply to over email, but your email address seems to unreachable from Microsoft (?)

Unfortunately, I can’t personally deliver a directed training for one company. But perhaps someone in the Spec Explorer team can help you or provide alternatives.

Best,

Nico

Answer 10

Hi Ignacio,

I had the same problem as Nico and couldn't reach your email address. Do you have an alternative one that we can use?

Thanks,

Spec Explorer Team.

Answer 11

Hi All,

Another excellent introduction focusing on the principles by Edward A. Lee and Sanjit A. Seshia can be found here: http://leeseshia.org/.
The chapters 3,5,13 etc. are valid for nearly all systems (i.e. not just embedded).
Some definitions are different, but the introduction is essential and another good starting point for understanding "what is under the hood".