Model-based Testing of a Software Bus - Applied on Core Flight Executive

1© 2014 Fraunhofer USA, Inc.
Center for Experimental Software Engineering
Model-based Testing of a Software Bus
applied on Core Flight Executive
Dharmalingam Ganesan, Mikael Lindvall
Dave McComas (NASA GSFC)
Presented at Flight Software Workshop, Pasadena, CA, 2014

Traditional Test Automation
 Only test execution is automated
 E.g. Junit, CuTest, etc.
 Test cases are manually constructed
 Effort intensive
 Some issues with traditional testing:
 Insufficient coverage of off-nominal behaviors
 Tests are too-detailed with low-level details
 Not easy to test multi-tasking architecture
 More on this later.

Model-based Testing (MBT)
 The tester develops a model (a.k.a. testing models)
 instead of writing suite of test cases
 The model becomes the test oracle
 Test cases are auto-generated from the model
 based on requirements, API documentations
 Key benefits:
 Tester works at a high-level of abstraction
 Innumerable number of test cases derived from the model
 Triggers many, if not all, off-nominal behaviors
 Precise specification

System under test (SUT)
• The Core Flight Software System (CFS)
• a mission-independent, platform-independent, Flight
Software (FSW) environment integrating a reusable core
flight executive (cFE)
• The CFS is a product-line developed by the NASA
Goddard Space Flight Center (GSFC)
• CFS is implemented in C
• cFE layer of the CFS is open source

cFE/CFS Context Diagram
Inter-task Message Router (SW Bus)
Transponders
Commands
Real-time Telemetry (UDP)
Comm Cards
File downlink
(CFDP)
Summit Chip
Mass
Storage
System
CFDP File
Transfer
File
Manager
Local
Storage
Data
Storage
Event
Services
Executive
Services
Time
Services
1553 Bus
Support
Software
Bus
Command
Ingest
Telemetry
Output
Table
Services
EDAC
Memory
Scrubber
Self
Test
Memory
Dwell
Instrument
Manager
Checksum
Memory
Manager
GN&C
Applications
(4)
Mission Apps
cFE core App
CFS Applications
Stored
Commanding
Software
Scheduler
Health &
Safety
Manager
House-
keeping
Limit
Checker

MBT of Software Bus
 cFE has a software bus (SB)
 Apps communicate indirectly using the SB
 Publish-Subscribe architectural style
 SB has unit-tests (developed by NASA GSFC)
 Good coverage but
 not taking multi-tasking into consideration
 Goals: find defects related to multi-tasking (difficult!)
 Generate test cases for SB
 Generate the “bubbles” (the apps on previous slide)
 Demonstrate the applicability of MBT
 Developed an approach of testing SB
 Allows testing of multi-tasking architectures

Scope of the current model
 Modeled the following behaviors
 Create Pipes (to hold messages)
 Delete Pipes
 Subscribe to Messages
 Send Messages
 Receive Messages
 Multiple Apps (dynamically instantiated)
 Innumerable test cases (in C) auto-generated
 Model based on Microsoft’s Spec Explorer Tool
 Will get back to this

Challenges of testing a SB
 To test a SB we need apps that publish-subscribe
 Apps are runtime tasks that communicate using the
SB
 Apps publish/subscribe to messages
 Each app cannot decide on its own the correctness
 Correctness depends on the global state of the system
 E.g: subscribe(msg), RecvMsg() may not work if no other
task is publishing any message
 The order of execution of tasks also matters
 Need a test architecture!

Test Architecture – Key Ideas
 Parent/Child architecture for testing
 Each test case is a parent
 Each test case runs as an app
 At run-time, one or more child tasks are spanned by
the parent
 Model controls the behavior of the parent
 All test assertions are decided by the parent
 All child tasks share the codebase
 How the parent and children communicate?
 Why not just use the software bus itself?

Test Architecture
CFE
Paren
t
Child
1
Child
2
Child
n
Command Pipe
All child tasks share the codebase

Test Architecture – Key Ideas
 Each child task subscribes to all commands, such as
Create Pipe, Delete Pipe, Subscribe, etc.
 Parent broadcast commands to all child tasks
 Communication uses CFE infrastructure
 Task id of the child is also part of the message struct
 Only the target child can perform a certain command
 Child tasks perform the command and send the
return code back to the parent
 Child tasks send out a result msg
 Parent task subscribes to the result msg
 The parent verifies test assertion
 Asserts are generated from the model

Spec Explorer – Brief Background
 Tester develops a model (a.k.a. model program)
 Spec Explorer runs as a plug-in to MS Visual Studio
 Model programs are written in C# like syntax
 The model program is a simplified version of the
SUT
 Spec Explorer generates state machines from
models
 Also checks whether model satisfies invariants
 Helps in validating the model
 Test cases are automatically derived from state
machines
 SUT’s behavior is automatically compared with
model

Abstractions for the model program
 Model program is another implementation of the
SUT
 But we do not want to create two implementations
 No one wants to maintain two implementations
 No one wants to develop a system two times
 How did we create a simplified version of the SUT?
 Key idea: Apply abstractions
Model of GPM, which uses CFE

Sample abstractions for a model
 Model is agnostic to multi-tasking complexity of the
SB
 Model has a very simple message structure
 Message is modeled as an int (not C structures)
 Message queues/pipes are also abstracted
 Finite depth
 Message queues are modeled as simple sequences
 instead of using shared memory
 No pointers, threads, semaphores at the model level
 Very simple data structure using very basic data types
 int, boolean, maps

Structure of the model program
E.g.: Number of apps, pipes
Represent the state of the bus
Used for excluding the uninteresting states
Which states are good for terminating tests
Models the actual logic of the software bus
Preconditions for enabling the rule methods to fire
Generates values for rule method
Utilties for rule methods and guards

State Data

Fragments of the model program
Rules are enabled only if Condition.IsTrue returns true

Fragments of the guards

Slicing the model for specific tests

Generated from the model program
We generate
the model!
In “regular”
MBT you have
to manually
create the
model.

Generated test sequences - sample
Each chain is a test case

SUT Adapter
 Adapter wraps the SUT
 Converts data/commands from the model into SUT’s
syntax
 Adapter simplifies modeling complexity
 Methods of the model should map to the adapter
 Our adapter is in C#
 We “print” test code from our adapter in C
 Converts C# tests into C tests
 Recall that CFE’s SB interface is in C

Our abstracted interface for Testing
int32 InitApp_w(int32 appName);
int32 CreatePipe_w(int32 appName, int32 pipeName, int32
pipeDepth);
int32 DeletePipe_w(int32 appName, int32 pipeName);
int32 Subscribe_w(int32 appName, int32 msgId, int32 pipeName);
int32 UnSubscribe_w(int32 appName, int32 msgId, int32
pipeName);
int32 RcvMsg_w(int32 appName, int32 pipeName, int32*
actualMsgId);
int32 SendMsg_w(int32 appName, int32 msgId);

Sample generated test case
void Parent_TestAppMain( void ) {
int32 status;
uint32 RunStatus = CFE_ES_APP_RUN;
Parent_TestAppInit();
status = InitApp_w(APP_0);
assert(status == CFE_SUCCESS);
status = CreatePipe_w(APP_0, PIPE_0, 1);
status = Subscribe_w(APP_0, MSG_0, PIPE_0);
status = Subscribe_w(APP_0, MSG_1, PIPE_0);
status = UnSubscribe_w(APP_0, MSG_1, PIPE_0);
CFE_ES_ExitApp(RunStatus);
}

Advantages of using Model-Based Testing
 The model focuses on the domain (easier to
understand)
 Instead of being source code oriented (harder to
understand)
 We automatically generate an endless number of
executable test cases (high coverage)
 Instead of manually writing individual test cases
 The information is in one place: in the model, easy to
maintain
 Instead of being spread out (hard to maintain)
 The test cases can easily be run over and over again

Advantages of using Spec Explorer
 Generated tests are pretty readable
 This is due to the ability to slice models into smaller
models
 Data parameters are well handled
 E.g., Model can be configured to test multiple apps
 Models are programs
 Ideal for programmers (who prefer coding)
 Models can be formally verified
 Invariants encoded in the model help to validate the
model

Challenges with Spec Explorer
 Modeling errors can lead to infinite state machine
 Need to be careful even for small models (e.g., int
parameters)
 Syntax for slicing the model is powerful but not that
easy
 Easy to misuse some of (algebraic) operators for slicing
 Completeness of our slices
 Did we miss any combination of behaviors during slicing?
 Model debugging. For example:
 Why a new state was generated?
 Where/Why the invariants are violated?

Applicability to other flight software
 The same approach is applicable to other types of
sw
 Requirements are that
 The software has an interface (e.g. API, GUI)
 Through which commands (stimuli) can be sent
 Through which results (responses) can be received
 Need (some) specification
 Optional: Sample test cases, API usage examples

Conclusion
 MBT works well for testing of multi-tasking
architecture
 In this case of a software bus
 Parent/Child test architecture facilitates testing
 Individual tasks cannot decide correctness of their own
 Parent coordinates with children and asserts correctness
 Models and generated state machines: a good spec!
 Innumerable number of test cases from the model
 Test cases are agnostic to cFE syntax but still executable
 Need to be careful in managing the model’s
complexity
 Abstraction is important
 Otherwise the model will be as complex as the system under

Acknowledgement
 Jan-Philip Quirmbach (Fraunhofer Intern)
 cFE is open source – not an issue for foreign interns
 Alan Cudmore (NASA GSFC)
 OSMA SARP:
 Martha Wetherholt (NASA HQ)
 Ken Rehm (NASA IV&V)
 Ricky A. Forquer (NASA IV&V)
 This work was partly funded by SARP

Questions
 Dharma Ganesan (dganesan@fc-md.umd.edu)

Model-based Testing of a Software Bus - Applied on Core Flight Executive

Recommended

More Related Content

What's hot (20)

Viewers also liked (13)

Similar to Model-based Testing of a Software Bus - Applied on Core Flight Executive (20)

More from Dharmalingam Ganesan (20)

Recently uploaded (20)

Model-based Testing of a Software Bus - Applied on Core Flight Executive