Commit 3493b89e authored by Ludovic Apvrille's avatar Ludovic Apvrille

Update on code generation: adding orderscheduler

parent 4352e45e
This diff is collapsed.
......@@ -140,6 +140,15 @@ public class TMLArchitecture {
return false;
}
public boolean hasHwExecutionNode() {
for (HwNode node : hwnodes) {
if ((node instanceof HwCPU)|| (node instanceof HwA)|| (node instanceof HwFPGA)) {
return true;
}
}
return false;
}
public boolean hasBus() {
for (HwNode node : hwnodes) {
if (node instanceof HwBus) {
......
......@@ -190,7 +190,7 @@ public class TMLMapping<E> {
tmla = new TMLArchitecture();
}
if (!tmla.hasCPU()) {
if (!tmla.hasHwExecutionNode()) {
cpu = new HwCPU("defaultCPU");
cpu.byteDataSize = 4;
cpu.pipelineSize = 1;
......
......@@ -185,7 +185,7 @@ public class DiploSimulatorCodeGenerator implements IDiploSimulatorCodeGenerator
header += "#include <PropRelConstraint.h>\n#include <SeqConstraint.h>\n#include <SignalConstraint.h>\n#include <TimeMMConstraint.h>\n";
header += "#include <TimeTConstraint.h>\n";
header += "#include <CPU.h>\n#include <SingleCoreCPU.h>\n#include <MultiCoreCPU.h>\n#include <FPGA.h>\n#include <RRScheduler.h>\n#include " +
"<RRPrioScheduler.h>\n" + "#include <PrioScheduler.h>\n#include <Bus.h>\n";
"<RRPrioScheduler.h>\n" + "#include <OrderScheduler.h>\n" + "#include <PrioScheduler.h>\n#include <Bus.h>\n";
header += "#include <Bridge.h>\n#include <Memory.h>\n#include <TMLbrbwChannel.h>\n#include <TMLnbrnbwChannel.h>\n";
header += "#include <TMLbrnbwChannel.h>\n#include <TMLEventBChannel.h>\n#include <TMLEventFChannel.h>\n#include <TMLEventFBChannel.h>\n";
header += "#include <TMLTransaction.h>\n#include <TMLCommand.h>\n#include <TMLTask.h>\n";
......@@ -273,10 +273,7 @@ public class DiploSimulatorCodeGenerator implements IDiploSimulatorCodeGenerator
final HwFPGA hwFpgaNode = (HwFPGA) node;
final String schedulerInstName = namesGen.rrSchedulerInstanceName(hwFpgaNode);
final String schedulerName = namesGen.rrSchedulerName(hwFpgaNode);
declaration += "RRScheduler* " + schedulerInstName + " = new RRScheduler(\"" + schedulerName + "\", 0, " + (tmlmapping
.getTMLArchitecture().getMasterClockFrequency() * HwA.DEFAULT_SLICE_TIME) + ", " + (int) Math.ceil((float) (hwFpgaNode
.clockRatio * Math.max(hwFpgaNode.execiTime, hwFpgaNode.execcTime) * (HwA.DEFAULT_BRANCHING_PREDICTION_PENALTY * HwA
.DEFAULT_PIPELINE_SIZE + 100 - HwA.DEFAULT_BRANCHING_PREDICTION_PENALTY)) / 100) + " ) " + SCCR;
declaration += "OrderScheduler* " + schedulerInstName + " = new OrderScheduler(\"" + schedulerName + "\", 0) " + SCCR;
final String hwFpgaInstName = namesGen.hwFpgaInstanceName(hwFpgaNode);
......
......@@ -16,6 +16,23 @@
<![endif]-->
</head>
<body>
<p>Avatar targets the design of embedded software</p>
<h1 id="introduction">Introduction</h1>
<p>AVATAR stands for Automated Verification of reAl Time softwARe. AVATAR targets the modeling and formal verification of the software of real-time embedded systems.</p>
<h2 id="diagrams">Diagrams</h2>
<p>The AVATAR profile reuses eight of the SysML diagrams (Package diagrams are not supported). AVATAR supports the following methodological phases:</p>
<ul>
<li><p><em>Requirement capture</em>. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.</p></li>
<li><p><strong>Assumption modeling</strong>. Assumptions of system may be captured with an assumption modeling diagram, based on a SysML requirement diagram.</p></li>
<li><p><strong>System analysis</strong>. A system may be analyzed using Use Case Diagrams, Activity Diagrams and Sequence Diagrams.</p></li>
<li><p><strong>Software design</strong>. Software is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines.</p></li>
<li><p><strong>Property modeling</strong>. The formal semantics of properties is defined within TEPE Parametric Diagrams (PDs). Since TEPE PDs involve elements defined in system design (e.g, a given integer attribute of a block), TEPE PDs may be defined only after a first system design has been performed.</p></li>
<li><p>**Software deploiement* is performed with UML deploiement diagrams</p></li>
</ul>
<h2 id="verifications">Verifications</h2>
<ul>
<li><p>Formal verification can be performed from software design. Formal verification relies on internal tools (e.g. internal model-checker, reachability graph generator, graph minimization, test sequences generation) or UPPAAL.</p></li>
<li><p>Simulation can be performed from deploiement diagram. It relies on the SoCLib environment.</p></li>
<li><p>Executable code generation can be performed from software design diagrams. Code is generated in C/POSIX format.</p></li>
</ul>
</body>
</html>
Avatar targets the design of embedded software
\ No newline at end of file
# Introduction
AVATAR stands for Automated Verification of reAl Time softwARe. AVATAR targets the modeling and formal verification of the software of real-time embedded systems.
## Diagrams
The AVATAR profile reuses eight of the SysML diagrams (Package diagrams are not supported). AVATAR supports the following methodological phases:
- *Requirement capture*. Requirements and properties are structured using AVATAR Requirement Diagrams. At this step, properties are just defined with a specific label.
- **Assumption modeling**. Assumptions of system may be captured with an assumption modeling diagram, based on a SysML requirement diagram.
- **System analysis**. A system may be analyzed using Use Case Diagrams, Activity Diagrams and Sequence Diagrams.
- **Software design**. Software is designed in terms of communicating SysML blocks described in an AVATAR Block Diagram, and in terms of behaviors described with AVATAR State Machines.
- **Property modeling**. The formal semantics of properties is defined within TEPE Parametric Diagrams (PDs). Since TEPE PDs involve elements defined in system design (e.g, a given integer attribute of a block), TEPE PDs may be defined only after a first system design has been performed.
- **Software deploiement* is performed with UML deploiement diagrams
## Verifications
- Formal verification can be performed from software design. Formal verification relies on internal tools (e.g. internal model-checker, reachability graph generator, graph minimization, test sequences generation) or UPPAAL.
- Simulation can be performed from deploiement diagram. It relies on the SoCLib environment.
- Executable code generation can be performed from software design diagrams. Code is generated in C/POSIX format.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment