# Presentation: 565125

## Getting Somewhat Formalwith CSP and C++

*Bill** Gardner**, Assoc. Prof.*
- Modeling & Design Automation Group
- Dept. of Computing & Information Science
- University of Guelph

- LFM

- 30/APR/08

## Outline

- Overview of “selective formalism”
- Based on **CSP++** tool set:Making CSP specifications executable in C++
*Communicating Sequential Processes (Hoare)*
- Case studies: focus on ATM
- Technical look:
- extent of CSP support; runtime mechanism
- Current status/availability; future work

- LFM

- 30/APR/08

## “Spectrum” of Formality

- Mature,repeatable devpt process

- Ad hoc“Gonzo”SW devpt

- Full formaldevelopment

- Use offormalspecifications

**Selective****formalism**

- Remove ambiguities
- Prove properties
-  Relies on hand-    translation to code

- Prove properties
- Code provably    equivalent to specs
-  Relies on gurus to    write specs, pilot    refinements to code

- LFM

- 30/APR/08

## Selective Formalism

- Formal spec (CSP) for “control backbone”
- Interprocess communication/synchronization
- Most vulnerable to concurrency snares:
*Deadlock, livelock, safety issues*
- Prove properties
- Automatic code generation  C++
- Plug in non-formal C++ modules
- Invoked by CSP events & channels

- LFM

- 30/APR/08

## Concurrent programming

- IPC = rich source of faults
- Programmers choose among techniques: mutexes, semaphores, monitors, (conditional) critical regions, condition variables
- May not appear in programming language directly→cobble together
- Must apply correctly “or else”
- Lock/unlock mutexes in right order, etc.
- Faults hard to reproduce, order dependent

- LFM

- 30/APR/08

## Sample of CSP:Vending Machine

- SYS = CUST [|{|insert,select,get|}|] VEND(0)
- CUST = insert!100 → insert!25 →select!RootBeer → get.RootBeer → SKIP
- VEND(dep) = insert?amt → VEND(dep+amt)[]
- 	select?prod → get.prod → VEND(0)

- LFM

- 30/APR/08

## What CSP buys you

- Simple, small set of IPC elements:
- CSP synchronization = rendezvous (barrier)
- CSP channel characteristics:
- One-way communication
- Point-to-point (broadcast possible)
- Unbuffered
- Avoids usage errors of other IPC techniques
*Except:* circular waiting (deadlock) possible

- LFM

- 30/APR/08

## Automated CSPm Tools

- Different ways to explore your CSP spec before you go to code:
- From Formal Systems (Europe) Ltd: ProBE
- Process exploration tool, expands any CSP statement, treelike, to all reachable states
- Make sure your CSP does what you thought

- LFM

- 30/APR/08

## Verification of properties

- Another Formal Systems tool, FDR2
- “Failures Divergences Refinement”
- Checks for deadlocks automatically
- Done by state-space exploration, sped up by heuristics
- Refinement checking
- Safety properties verification

- LFM

- 30/APR/08

## Selective Formalism

- System designers decide:
- How much of system to specify in CSP
- Control backbone
- Critical areas
- How much to write in conventional C++
- Computations, I/O
*NO* interprocess comm/sync (breaks formal model)
- Limits role of formal gurus:
- Spec writing, verification

- LFM

- 30/APR/08

## Bridging the formal method vs. implementation gap

- _CSP_
- formal “backbone”
- models control structure
- interprocess sync/comm
- verification tools

- _C++_
- plug-in modules
- bulk of data processing
- restrictions (no IPC)

- LFM

- 30/APR/08

## Layered System Model

**CSP++ Control Layer**

**Hardware** **Components**

**RTOS** **Facilities**

**Packages**

**User-coded**
**Functions**

- Target System

- LFM

- 30/APR/08

## CSP++ Design Flow

**User**
**Functions**

**CSP Specs**

- LFM

- 30/APR/08

## Integration of User Code

**Hardware** **Components**

**RTOS** **Facilities**

**Packages**

**External Event**
**Routines**

**CSP++ Control****Layer**

- P2

- P3

- P1

- f1

- f3

- f4

- f2

- P1

- CSP process

- CSP event

- f1

- user function

- LFM

- 30/APR/08

## Restrictions on User Code

- Can link to individual events, or multiple cooperating events of leaf-level process
- Cannot rely on static storage (due to multiple process instances) except as provided by framework
- Cannot “go behind back” of CSP spec to contact other processes
- preserves convention that interprocess communication/synchronization done via CSP

- LFM

- 30/APR/08

## What can you do with CSP++?

- Case studies to date:
- Disk controller (performance benchmark)
- Point-of-sale terminal [Carter & Xu 2005]
- Targets Xilinx Microblaze processor core onVirtex-II FPGA
- Automated teller [Doxsee & Gardner 2005]
- With 22 user-coded functions
- Network interface to simulated bank using MySQL
- Robot probe [Carter & Gardner 2007]

- LFM

- 30/APR/08

## CSPm for one ATM process

- LFM

- 30/APR/08

## Sample Translation of CSPm by cspt to C++

- LFM

- 30/APR/08

## Sample User-coded C++ Function

- linked to the CSPm channel readpin?p
- obtains PIN and returns it via status

- LFM

- 30/APR/08

## ATM Performance Metrics

- 1.5 GHz Pentium M, 512 Mb RAM
- UCFs removed so only framework overhead measured
- 10,000 ATM transactions
- Compared with commercial SW synthesis tool, Rational Rose RealTime V6.5
- Generates C++ from UML state diagrams

- LFM

- 30/APR/08

## ATM Timing

- Learned:
- Structure of CSPm spec strongly influences run-time performance (environment stack, threads)
- Pth is slow compared to native POSIX threads

| 10,000 transactions | Total Secs. |
| --- | --- |
| RRRT V6.5 | 4.92 |
| CSP++ original CSPm | 19.8 |
| CSP++ flattened CSPm | 8.45 |

- LFM

- 30/APR/08

## Contrast Component Kit Approach

- Construct executable system from library of components with CSP semantics
- E.g., JCSP/CCSP/C++CSP
- Appropriate for *static* process structure
- Event/channel renaming not applicable
- [Raju et al 2003] Translates CSPm to CTJ, JCSP, CCSP
- CSP++ does more operators

- LFM

- 30/APR/08

## Process Definitions

- Simple:			M = a -> b-> SKIP
- Parameterized:	P(1,n) = ch!n -> Q				P(x,n) = R(x) ||| S(n)
- Translation-time vs. run-time binding
- ... -> M			... b?y -> P(y,4)
- ... -> P(1,5)

- LFM

- 30/APR/08

## Process Composition

- Interleaving:	P ||| Q ||| R
- Sequence:	P ; Q ; R
- Interface (sharing) parallel:    P[|*events*|]Q
- Simple event set: {a,b,c}
- Event closure: {|chan|}

- LFM

- 30/APR/08

## Supported Operators

- Comments: -- *and* {-...-}
- Prefix: ->
- I/O: 	ch.1.5!12 ... ch.1.5?z
- if ... then ... else
- External choice:	a->P [] b->Q
*Limitation: initial event must be exposed*
- Renaming: [[e<-f]]
- Hiding: \{e}

- LFM

- 30/APR/08

## OO Application Framework

- A given translated C++ program =a customization of the framework
- Most generated code instantiates OOAF classes
- Process; Channel; Event; etc.
- Classes incorporate CSP execution semantics
- Targeting OOAF shortens translation “distance” compared to directly generating assembly code & C++ OOAF more portable

- LFM

- 30/APR/08

## Run-time Environment Stack

- Branches at composition operators (tree)
- Records all...
- Synchronization sets (sync objects become “control center” for sync/comm in progress)
- Hiding & renaming
- Event execution searches up stack to identify sync/comm, apply hiding/renaming
- Trace printing reflects hiding/renaming
- Can verify that trace refines original spec

- LFM

- 30/APR/08

## Recent developments (1)

- Added synthesis of *Timed CSP* operators to CSP++
- Original CSP is untimed
- Timed CSP adds delays ***-d->***, timeouts **[*****d*****>**, and timed interrupts **/*****d*****\ **(+untimed versions [> /\ )
- Recent tool for carrying out timed verification:
- HORAE, National Univ. of Singapore
- Includes robot vacuum case study

- LFM

- 30/APR/08

## Recent developments (2)

- New **Eclipse plug-in **for CSP++
- CSP-highlighting specification editor
- Integrated with Formal Systems tools (ProBE, FDR2) and maybe HORAE
- One-click translation/build
- Export execution trace to FDR for verification
- Convenient integration of C++ user-coded functions
*Goal:* Make CSP++ attractive for use in education
- Help automate, smooth design flow

- LFM

- 30/APR/08

## Future work

- More data types (only int now)
- Extend CSP channels/events to coprocessor
- Target digital logic on FPGA, SOPC
- Add hardware synthesis to cspt translator
- Hardware/software codesign:
- Partition CSP spec: SW part→C++ source code
- HW part→HW description language → FPGA netlist
- Synthesize the communication links between them

- LFM

- 30/APR/08

## Future work (2)

- Concise training for roles:
**CSPm “guru”:**
- write CSPm, write assertions, run verification tools
- System designers identify named CSP events to be linked with C++ functions
- I/O, interface to external components, calculations
**UCF coder:** write C++, test/debug system
*How much CSP knowledge is enough?*

- LFM

- 30/APR/08

## Availability

- Formal Systems tools (ProBE, FDR) free fornon-commercial use (www.fsel.com)
- CSP++ also free
- Only needs GNU g++ and Pth portable threads
- Threading model is non-preemptible without priorities

- LFM

- 30/APR/08

## CSP++ Versions

- Download from my website:www.cis.uoguelph.ca/~wgardner“Research & Downloads” link
- V4.1 binaries available now + case studies code
- V4.2 soon to be released as “open source”
- Will include Eclipse plug-in
- V5.0 with timed operators still in testing

- LFM

- 30/APR/08

## Conclusion

- CSP++ makes *synthesizable subset* of verifiable CSPm specifications executable & extensible
- Tool for carrying out *selective formalism *with user-coded C++ functions
- Possibility of making (some) formalism more palatable & practical to the resistant

- LFM

- 30/APR/08

## Slide 35

- 30/APR/08

## Utilize 4 kinds of CSP

*Functional model:*
- Processes with desired system behaviour
*Environment model:*
- Processes simulate entities interacting with system
*Constraint model:*
- Optional processes limit/constrain event sequences (including safety properties)
*Implementation model:*
- Detailed functionality for synthesis

- LFM

- 30/APR/08

## Refinement checking in FDR

- Does candidate implementation X “refine” specification S?
- Done by verifying traces(X)  traces(S)
- “Spec S is ‘trace refined’ by implementation X”
- Verify that traces output from CSP++ simulation refine original CSP spec!(have tool for this)

- LFM

- 30/APR/08

## Safety properties in FDR

- After given sequence of events, system should *not *engage in certain “unsafe” events
- Set up specification of a *bad* CSP process that you *don’t* want to occur
- Check whether it refines original spec
- If not, proves the spec is *safe* (in that regard)

- LFM

- 30/APR/08

## Prospects for adoption

- Realistically, groundwork for industry practice laid in university education today
- Where are formal methods in our/anyone’s undergrad curriculum?
- Suitable for 4th yr/grad course
- 50% exposure to variety of methods
- 50% concentrate on actually using one

- LFM

- 30/APR/08

- Related work: libraries approach
- Since manually assembled, not “correct by construction”
- Suitable for specs with static process structure (no renaming, hiding, little/no dynamic process creation)
- Tech’l: CPA talk
- ATM: CPA talk

- LFM

- 30/APR/08