Dans ce module/semaine, vous apprendrez à dessiner un modèle de système de consommation/production de jetons et à communiquer votre interprétation de ce modèle avec d'autres personnes de manière informelle. A la fin de ce modèle, vous serez capable de dessiner vos propres modèles et d'expliquer votre interprétation en termes généraux. Vous connaîtrez également l'interprétation standard des réseaux de Petri des systèmes de consommation/production et serez en mesure de mettre en évidence des schémas particuliers dans les modèles de réseaux de Petri. Enfin, vous serez en mesure d'affiner un modèle de consommation/production en un modèle contenant suffisamment d'informations pour permettre une analyse des performances dans le pire des cas. Tout cela est testé à l'aide d'un travail évalué par des pairs.

Dans ce module/semaine, vous allez vraiment entraîner vos capacités de raisonnement abstrait. À l'issue de ce module, vous aurez appris à formaliser le comportement de tout système dynamique sous la forme d'un ordre préfixe, et à formaliser l'interprétation d'un système de consommation/production sous la forme d'une fonction de comptage sur un tel ordre préfixe. Vous comprenez comment l'interprétation Petri-net impose certaines restrictions sur ces fonctions de comptage, et comment vous pouvez exploiter ces restrictions pour prouver des propriétés sur les interprétations Petri-net, sans connaître l'interprétation elle-même. A la fin du module, vous pratiquerez la formalisation des mesures de performance en tant que propriétés logiques des fonctions de comptage, en reconnaissant les bons et les mauvais exemples de formalisation. Ceux qui sont déjà familiers avec la théorie des réseaux de Petri trouveront peut-être que la sémantique de l'ordre préfixe que j'introduis dans ce cours est légèrement différente de celle à laquelle ils sont habitués. La sémantique traditionnelle des réseaux de Petri est généralement basée sur les marquages, les systèmes de transition ou les arbres d'exécution qui en découlent. Les arbres d'exécution sont un exemple particulier d'ordre préfixe, mais en général, les ordres préfixes offrent la flexibilité supplémentaire de ne pas restreindre l'utilisateur à des interprétations discrètes du comportement. Ceci est particulièrement approprié lorsque l'on cherche à établir un lien entre l'informatique théorique et un domaine d'application tel que les systèmes embarqués, dont ce cours est issu, où le comportement continu des systèmes physiques doit également être pris en compte.

Dans ce module/semaine, vous apprendrez à exploiter la structure des graphes de flux de données à taux unique pour effectuer l'analyse la plus défavorable des mesures de performance telles que le débit, la latence et la mise en mémoire tampon. Après cette semaine, vous savez comment calculer la moyenne du cycle maximum d'un graphe de flux de données, comment construire un programme périodique pour celui-ci, comment optimiser ce programme pour l'analyse de la latence, et comment déterminer la taille des tampons avec la contre-pression de telle sorte que l'analyse du pire cas reste valide. Si vous avez compris la matière du module/semaine précédent, les preuves présentées dans cette semaine vous permettront de mieux comprendre les fondements mathématiques de ces méthodes.

Au cours de cette dernière semaine, nous discutons d'un exemple supplémentaire, en suivant les grandes lignes du travail évalué par les pairs du premier module/semaine. Il s'agit juste d'un petit résumé, combinant tout ce que nous avons appris jusqu'à présent, et il y a quelques lectures supplémentaires pour susciter l'envie d'aller plus loin dans la découverte.