Transcript Software Engineering - The Information and Telecommunication

Engineering of Computer-Based
Systems
Dr. Perry Alexander
Associate Professor
[email protected]
http://www.ittc.ukans.edu/~alex
Information and Telecommunications
Technology Center
The University of Kansas
Applied Formal Methods
Applied Formal Methods
Using Modeling to
Develop Reliable Systems
A Problem to solve, but how?
First, define the problem...
Mathematics defines precisely
x:T•P(x) /\ Q(x) /\ R(x) ...
…then, design the solution,...
x:T•P(x)=>z:T•Q(x,z) ...
Mathematical Modeling predicts behaviors
…build all the pieces...
{P1(x)}C1{Q1(x,z)}, {P2(x)}C2{Q2(x,z)} ...
Mathematics defines the pieces
…and assemble the system...
Ip(x)=>Ic(x) /\ Oc(x,z)=>Op(x,z)
Mathematics defines correctness
A Great Computer-Based
System
Information and Telecommunications
Technology Center
The University of Kansas
2
Modeling Projects
Network modeling, simulation and verification



Active Network performance simulation (DARPA)
Network security and information assurance (DARPA)
Active Network functional correctness (DARPA)
ASIC modeling and Verification


Pulse Interval Processor (TRW, AFRL)
Automated verification obligation generation and verification
(TRW, AFRL)
Simulation protocol modeling and verification

Time Warp distributed simulation verification (AFRL)
Information and Telecommunications
Technology Center
The University of Kansas
3
Systems Level Design
Systems Level Design
Integrating information
from multiple domains into
design decision making
P=10uW+5uW+...
Architecture x of CPU is
begin
x <= fir(y);
wait for x’event
end x;
X <= F(y) after 5us
Information and Telecommunications
Technology Center
The University of Kansas
4
Systems Level Design Projects
Rosetta language design and tool support






Systems level modeling language (AverStar, VHDL International,
AFRL, DARPA, NASA)
Automated Test Vector Generation (TRW, AFRL)
Mechanical system redesign demonstration (AFRL)
Bluetooth demonstration project ongoing (Texas Instruments,
AverStar)
Language Standardization to begin next year
http://www.sldl.org
VSPEC and VHDL modeling and verification


Pulse Interval Processor modeling and verification (TRW, AFRL)
Common Signal Processor modeling (TRW, AFRL)
Information and Telecommunications
Technology Center
The University of Kansas
5
Architecture and Component Reuse
IP Reuse
Reuse of existing software
and hardware components
Input
Component
Component
• Define components and their
interconnections in an architecture
• Verify the high level architecture
• Find component instances
• Use formal methods to match
components
• Use formal methods to adapt
components
• Component reuse with confidence!
Component
Information and Telecommunications
Technology Center
Output
The University of Kansas
6
Component Reuse and Retrieval
Component reuse system


Retrieval and reuse of VSPEC annotated VHDL designs
(DARPA)
Retrieval and reuse of Rosetta annotated system
components (EDAptive Computing, DARPA)
Legacy component and replacement

Retrieval and reuse of components based on match with
existing legacy systems (EDAptive Computing, ONR)
Information and Telecommunications
Technology Center
The University of Kansas
7
Other Activities…
Commercialization efforts


Rosetta – Accellera, Texas Instruments, Averstar and many others…
Component Retrieval and Reuse – EDAptive Computing, TRW and
others…
Vice Chair, IEEE Engineering of Computer-Based Systems
Engineering TC
Member, IEEE Design Automation Standards Committee
Chair, Accellera SLDL Language Subcommittee
Member, DARPA 21st Century Engineering Consortium on Formal
Methods Education
Information and Telecommunications
Technology Center
The University of Kansas
8