Bonjour à tous,

Nous avons le plaisir de vous inviter au dixième séminaire de la session d'hiver 2021 du LATECE. 

Lieu: Zoom : https://uqam.zoom.us/j/85977067999

Titre :Spécification et vérification de contrat: Expérience avec le langage Symboleo

Conférencier :Daniel Amyot

Title : Contract Specification and Verification: Experience with the Symboleo Language

Résumé : Les contrats légaux précisent les conditions qui s'appliquent aux transactions commerciales. Les contrats sont généralement exprimés en langue naturelle et contiennent de nombreuses exigences juridiques qui sont souvent ambiguës, incomplètes et même incohérentes. Les contrats intelligents sont des programmes destinés à automatiser, surveiller et contrôler partiellement l'exécution des contrats légaux afin de garantir le respect des conditions générales pertinentes. Cette présentation se concentre sur la spécification formelle de contrats légaux qui permet une analyse automatisée et éventuellement la génération de contrats intelligents programmés qui surveilleront l’exécution des contrats légaux initiaux. À cette fin, le langage de spécification textuel Symboleo a été récemment proposé, où les contrats sont composés d'obligations et de pouvoirs qui définissent les exécutions conformes d'un contrat légal. Symboleo propose également des opérations modifiant l’exécution d’un contrat telles que la sous-traitance et la substitution. Les concepts sous-jacents à Symboleo sont spécifié par une ontologie dont la sémantique est décrite en termes d'axiomes logiques correspondant à des diagrammes d'état qui décrivent les cycles de vie des contrats, des obligations, des pouvoirs et autres concepts. Un codage des spécifications Symboleo dans le langage nuXmv, comprenant une bibliothèque de modules correspondant aux concepts de base de Symboleo, permet la vérification formelle des propriétés d'un contrat, exprimées en logique temporelle (LTL ou CTL). Des exemples et des retours d’expérience dans deux domaines (chaîne d'approvisionnement alimentaire et marchés d'énergie transactive) seront discutés, de même que les travaux en cours sur la surveillance des contrats et autres défis. 

Biographie : Daniel Amyot est Professeur à l'École de science informatique et de génie électrique de l'Université d'Ottawa, qu'il a jointe en 2002 après avoir été chercheur senior chez Mitel Networks. Il a publié plus de 200 articles en ingénierie des exigences, en génie logiciel, en modélisation, en conformité réglementaire et en informatique de la santé. De 2002 à 2013, il a dirigé l'évolution de la norme "User Requirements Notation" comme Rapporteur associé à l'Union Internationale des Télécommunications. Il s’investit maintenant dans le développement du langage Symboleo pour la spécification, la vérification et le suivi des contrats légaux et intelligents. Il détient un doctorat et une maîtrise en informatique de l'Université d'Ottawa (2001 et 1994) ainsi qu'un baccalauréat en informatique de génie de l'Université Laval (1992). Daniel est aussi membre du comité éditorial des revues SoSyM, REJ, et EMSE, président du comité aviseur de la conférence Requirements Engineering (RE), président de la SDL Forum Society, membre senior de l’IEEE et chercheur à l'Institut du savoir Montfort et à l’Institut de recherche LIFE.