-
Notifications
You must be signed in to change notification settings - Fork 67
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Updated training material for 2020-11 release.
- Loading branch information
Showing
7 changed files
with
95 additions
and
0 deletions.
There are no files selected for viewing
Binary file not shown.
43 changes: 43 additions & 0 deletions
43
sysml/src/training/30. Verification/Verification Case Definition Example.sysml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
package 'Verification Case Definition Example' { | ||
|
||
part def Vehicle { | ||
attribute mass :> ISQ::mass; | ||
} | ||
|
||
requirement vehicleMassRequirement { | ||
subject vehicle : Vehicle; | ||
doc /* The vehicle mass shall be less than or equal to 2500 kg. */ | ||
|
||
require constraint { vehicle::mass <= 2500@[SI::kg] } | ||
} | ||
|
||
verification def VehicleMassTest { | ||
import Verifications::*; | ||
|
||
subject testVehicle : Vehicle; | ||
objective vehicleMassVerificationObjective { | ||
// The subject of the verify is automatically bound to 'testVehicle' here. | ||
verify vehicleMassRequirement; | ||
} | ||
|
||
action collectData { | ||
in part testVehicle : Vehicle = VehicleMassTest::testVehicle; | ||
out massMeasured :> ISQ::mass; | ||
} | ||
|
||
action processData { | ||
in massMeasured :> ISQ::mass = collectData::massMeasured; | ||
out massProcessed :> ISQ::mass; | ||
} | ||
|
||
action evaluateData { | ||
in massProcessed :> ISQ::mass = processData::massProcessed; | ||
out verdict : VerdictKind = | ||
// Check that 'testVehicle' statisfies 'vehicleMassRequirement' if its mass equals 'massProcessed'. | ||
PassIf(vehicleMassRequirement(vehicle => testVehicle, massActual => massProcessed)); | ||
} | ||
|
||
return verdict : VerdictKind = evaluateData::verdict; | ||
} | ||
|
||
} |
52 changes: 52 additions & 0 deletions
52
sysml/src/training/30. Verification/Verification Case Usage Example.sysml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
package 'Verification Case Usage Example' { | ||
import 'Verification Case Definition Example'::*; | ||
|
||
part def MassVerificationSystem; | ||
part def Scale; | ||
|
||
part vehicleTestConfig : Vehicle { | ||
// ... | ||
} | ||
|
||
verification vehicleMassTest : VehicleMassTest { | ||
subject testVehicle :> vehicleTestConfig; | ||
} | ||
|
||
part massVerificationSystem : MassVerificationSystem { | ||
perform vehicleMassTest; | ||
|
||
part scale : Scale { | ||
perform vehicleMassTest::collectData { | ||
in part :>> testVehicle; | ||
|
||
// In reality, this would be some more involved process. | ||
measurement = testVehicle::mass; | ||
|
||
out :>> massMeasured = measurement; | ||
} | ||
} | ||
} | ||
|
||
individual def TestSystem :> MassVerificationSystem; | ||
|
||
individual def TestVehicle1 :> Vehicle; | ||
individual def TestVehicle2 :> Vehicle; | ||
|
||
individual testSystem : TestSystem :> massVerificationSystem { | ||
timeslice test1 { | ||
perform action :>> vehicleMassTest { | ||
individual :>> testVehicle : TestVehicle1 { | ||
:>> mass = 2500@[SI::kg]; | ||
} | ||
} | ||
} | ||
|
||
then timeslice test2 { | ||
perform action :>> vehicleMassTest { | ||
individual :>> testVehicle : TestVehicle2 { | ||
:>> mass = 3000@[SI::kg]; | ||
} | ||
} | ||
} | ||
} | ||
} |
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.