Visio Interaction Analysis Tutorial

1846-1917 Buffalo Bill

Description

Requirements Specifications Interaction AnalysisBill MitchellSoftware and Systems Research LabsDepartment of ComputingMotorola UK Research LabsUniversity of SurreySunday, June 22, 2003Reality of Engineering Requirements Specifications• Rapid development of lightweight specifications• Specification by example scenarios• Poor coverage of scenarios• Disjoint engineering groups with little communication• Extreme pressure to ship on timeHence large number of defects only found in field testing2Motorola LabsResearch Project PilotFATCAT an internal tool, takes sets of scenarios (in e.g MSC notation):• analyse scenarios coverage• find conflicts• construct interesting FI testsCurrent Pilot coordinated by Motorola UK Research lab with:• UI Design Group • UI Software Tool Development Labs• System Architecture Group• Testing Group• Testing Tools Software Management Group• Requirements Specification Managers• EU 6th Framework STReP, Forming a consortium:3Motorola LabsStandard TechniquesInternal study of 200 TETRA MSC scenarios with Spin and standard MSC automata synthesis algorithms (Alur, Leue etc).Result:• state explosion• generated many “bogus” errorsTwo other Motorola Research Labs built POTS system with Switch in SDL for model checking with FDR. Result:• state explosion problems• only found conflicts when the algorithm directed towards error statesFor wireless telecomms specifications, standard model checking not always the right ...

Informations

• Publié par: Zyof
• Nombre de lectures: 20
• Langue: English

Extrait

Requirements Specifications Interaction Analysis

Bill Mitchell

Department of Computing

University of Surrey

Sunday, June 22, 2003

•

Specification by example scenarios

•

Rapid development of lightweight specifications

2 bs

Hence large number of defects only found in field testing

•

Extreme pressure to ship on time

•

Disjoint engineering groups with little communication

•

Poor coverage of scenarios

Mto aaLrolo  fo ytilaeRquReg inernegiEnitacsnoemirtsenpe Sfici

lo aaLsbMtoro

Current Pilot coordinated by Motorola UK Research lab with: • UI Design Group • UI Software Tool Development Labs • System Architecture Group • Testing Group • Testing Tools Software Management Group • Requirements Specification Managers

• EU 6th Framework STReP, Forming a consortium:

3 rceaPrh ecojPit  F tol ACTAna Ttni  Rse  CSM g.e ni( soi lyna•a ):ontitano ateklo , lotreanenarf scts os se urtsi tc stci noc• FngteI erntties irsoc voess ecan nd confl erage •fi sst

Standard Techniques

Internal study of 200 TETRA MSC scenarios with Spin and standard MSC automata synthesis algorithms (Alur, Leue etc). Result: • state explosion • generated many “bogus” errors

Two other Motorola Research Labs built POTS system with Switch in SDL for model checking with FDR. Result: • state explosion problems • only found conflicts when the algorithm directed towards error states

For wireless telecomms specifications, standard model checking not always the right approach

4 oMtoroalL bas

Purpose of MSC Specifications

Specs define Phase Transitions • Each phase describes a meaningful part of the overall operation of the system. • Each phase involves its own mini-protocol. • Each MSC shows how to move from one phase to another, via intermediate phases.

Activate Handset

Idle

Call Set-up

5

Call Queued

Allocate Resource

Call Progressing

MotoroalL bas

otMolor

D

call setup[B] _

call(B)

B

Sys

C

call_active[B,C]

_ [B, ] call active D

idle

accept(D) hang_up_on(C) ack_accept(D) disconnect(B)

call_active(B)

sb 6  aaL xEmalp,eC la laW ni  WIF0002 initfrg  pomerap

idle

ring(A,B)

hang_up_on(C)

rbwf(B)

A

_ p[B] call setu

call(B)

Sys

call_active[B,C]

B

ring(A,B)

rbwf_call_progressing[A,B]

xElpmaR ,eing Back When Free ,rfmop parei  20 W FIn  00 otoM Labrolas 7

call setup[B] _ call B

C

D

call_active[B,C]

rbwf(B)

call_active[B,C]

B

idle

call_active[B,D]

call_active(B)

accept(D) hang up_on(C) _ ack_accept(D) disconnect(B)

idle

Sys

call setup[B] _ call(B)

A

0002 WIpam ro f Finr peE 8 ax aLsb  ,IFpmel Mola otor

• Each instance to be implemented as a FSA

• Next state after each event is unique except where this causes nondeterminism

• FSA must be deterministic

• Phases define unique states in implementation

bs 9 loroaL atoM tic FSA implemenatitnoviaNeD emretsini

S2

S3

!c

S1 ?d

?c

S1 !d

S0 ?a ?b

FSA for B

S0 !a !b

FSA for A

A a c

S0

S2

S1

B

d

S3

S3

S2

B

S0

S1

A b

Dae 01 sbaL aloroot e M plamExk ocdl

Better Semantics?

• Each instance to be implemented as a DFSA • Phases correspond to set of states in DFSA (composite state) • Restrict construction of DFSA from MSC via additional semantics of phases.

a Labs 11 Motorol citsinimreteDntatleme imp FSAessP ahiwhtoi n