Lecture topics #112
MarkoSchuetz
started this conversation in
Ideas
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Here are some starting points from which you can derive tasks that would qualify as "lecture topics tasks".
These starting points are still quite generic and you can specialize and instantiate them.
UML sequence diagrams: you consider a scenario that involves several components (actors, objects,...) where describing the scenario in text alone is too awkward and becomes much easier with an accompanying diagram. You can create many instances of this particular task: whenever a developer or the manager feels that there is an non-trivial scenario that should be explained and that would be awkward to explain with text alone.
TLA+ (or Alloy, not yet discussed in class): if there is a fact that is important and not obvious (about the domain, about the requirements,...) you can model that part of the domain or the requirements and then claim the property/fact and let the model checker check that -at least in the model- that property holds. If the model checker finds a counterexample then that tells us either that the fact isn't true or that we might have overlooked some additional conditions/requirement/... For example, if we model a player with their score and the possibility to perform exercises, we might want to claim that the score cannot decrease. Let's say we've already modeled their score, an exercise's score, an initial state formula, and a state transition formula, but we've so far modeled the score of an exercise as an integer. If we state our property as an invariant: a player's score never decreases, then the model checker will find a trace in which there as an exercise that has a negative score and by doing this exercise the player's score goes down. So, we notice that it does not make any sense to have exercises with negative scores and we change our domain documentation or the requirements accordingly. This is certainly a contrived example, but it illustrates how we can apply TLA+ (or any other model checker like Alloy, mCRL2,...) to verify our understanding.
You can discuss your ideas for specific versions of these lecture topic tasks here in the discussion(s) or you can enter them directly in the project board if you think they are specific enough.
Beta Was this translation helpful? Give feedback.
All reactions