Disciplina Discipline MAC6966
Using Coq and CLEARSY safety platform in software industry

Using Coq and CLEARSY safety platform in software industry

Área de Concentração: 45134

Concentration area: 45134

Criação: 22/11/2019

Creation: 22/11/2019

Ativação: 22/11/2019

Activation: 22/11/2019

Nr. de Créditos: 1

Credits: 1

Carga Horária:

Workload:

Teórica

(por semana)

Theory

(weekly)

Prática

(por semana)

Practice

(weekly)

Estudos

(por semana)

Study

(weekly)

Duração Duration Total Total
5 5 5 1 semanas 1 weeks 15 horas 15 hours

Docentes Responsáveis:

Professors:

Flavio Soares Correa da Silva

Ana Cristina Vieira de Melo

Objetivos:

Métodos formais são técnicas matemáticas aplicadas ao desenvolvimento de software. Eles podem ser usados ​​no design, implementação, verificação e teste de sistemas. A aplicação de métodos matemáticos ao desenvolvimento de software é trabalhosa e propensa a erros. Devido a isso, muitas técnicas e ferramentas foram desenvolvidas para apoiar o desenvolvimento formal de software nas últimas décadas. Este curso é dedicado a mostrar o desenvolvimento formal de software na prática, usando ferramentas disponíveis no mercado e na academia.

Objectives:

Formal methods are mathematical techniques applied to software development. They can be used in the design, implementation, verification and testing of computer systems. Applying mathematical methods to software development is very labor intensive and error prone. Due to this, many techniques and tools have been developed to support the formal development of software in the last decades. This course is devoted to show the formal software development in practice, using tools available in the market and academia.

Justificativa:

A aplicação de métodos matemáticos no desenvolvimento de software torna-se muito difícil e cara sem o suporte de ferramentas apropriadas. Este curso tem como foco revisar o estado da arte em ferramentas que apóiam as abordagens formais de desenvolvimento de software.

Rationale:

The application of mathematical methods in software development becomes very difficult and expensive if no tool support is provided. This course is devoted to review the state of art in tools that support the formal software development approaches.

Conteúdo:

Existem duas abordagens principais na verificação formal de software: verificadores de modelos e provadores de teoremas. Na prática, eles podem ser usados ​​complementarmente. Neste curso, as duas abordagens serão introduzidas juntamente com ferramentas para mostrar como elas podem ser usadas no desenvolvimento de software. A utilização práticas das ferramentas também será mostrada, seguida de uma discussão sobre os benefícios e limitações de sua utilização no mercado.

Content:

There are two main approaches in the formal verification of software: model checkers and theorem provers. In practice, they can be used complementarily. In this course, both approaches will be introduced together with tools to show how they can be used in software development. The practical used of tools will also be shown, followed by a discussion on the benefits and limitations of using them in the market.

Forma de Avaliação:

Bibliografia:

Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (2005) Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010), http://www. cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569 Behm, P., Benoit, P., Faivre, A., Meynadier, J.: M et eor: A successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I. Lecture Notes in Computer Science, vol. 1708, pp. 369{387. Springer (1999), https://doi.org/10.1007/3-540-48119-2_22 Lecomte T., Burdy L. & Leuschel M. (2012):Formally Checking Large Data Sets in the Rail-ways.CoRRabs/1210.6815. Available at http://dblp.uni-trier.de/db/journals/corr/corr1210.html#abs-1210-6815. Lecomte, T., D eharbe, D., Prun, E., Mottin, E.: Applying a formal method in industry: A 25-year trajectory. In: da Costa Cavalheiro, S.A., Fiadeiro, J.L. (eds.) Formal Methods: Foundations and Applications - 20th Brazilian Sympo- sium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10623, pp. 70{87. Springer (2017), https://doi.org/10.1007/978-3-319-70848-5_6 Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verication, and Cer- tication - 1st Int'l Conf., RSSRail 2016, Paris, France, June 28-30, 2016, Proc. LNCS, vol. 9707, pp. 20{31. Springer (2016) Benjamin Pierce. Software Foundations series, Volume 1 - Logical Foundations, 2019. Available online: https://softwarefoundations.cis.upenn.edu/ Yves Bertot, Pierre Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. An EATCS Series, 2004.Available online: https://www.labri.fr/perso/casteran/CoqArt/ Adam Chlipala. Certified Programming with Dependent Types. The MIT Press, 2013. Available online: http://adam.chlipala.net/cpdt/

Bibliography:

Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (2005) Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010), http://www. cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569 Behm, P., Benoit, P., Faivre, A., Meynadier, J.: M et eor: A successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I. Lecture Notes in Computer Science, vol. 1708, pp. 369{387. Springer (1999), https://doi.org/10.1007/3-540-48119-2_22 Lecomte T., Burdy L. & Leuschel M. (2012):Formally Checking Large Data Sets in the Rail-ways.CoRRabs/1210.6815. Available at http://dblp.uni-trier.de/db/journals/corr/corr1210.html#abs-1210-6815. Lecomte, T., D eharbe, D., Prun, E., Mottin, E.: Applying a formal method in industry: A 25-year trajectory. In: da Costa Cavalheiro, S.A., Fiadeiro, J.L. (eds.) Formal Methods: Foundations and Applications - 20th Brazilian Sympo- sium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10623, pp. 70{87. Springer (2017), https://doi.org/10.1007/978-3-319-70848-5_6 Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verication, and Cer- tication - 1st Int'l Conf., RSSRail 2016, Paris, France, June 28-30, 2016, Proc. LNCS, vol. 9707, pp. 20{31. Springer (2016) Benjamin Pierce. Software Foundations series, Volume 1 - Logical Foundations, 2019. Available online: https://softwarefoundations.cis.upenn.edu/ Yves Bertot, Pierre Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. An EATCS Series, 2004.Available online: https://www.labri.fr/perso/casteran/CoqArt/ Adam Chlipala. Certified Programming with Dependent Types. The MIT Press, 2013. Available online: http://adam.chlipala.net/cpdt/

Tipo de oferecimento da disciplina:

Presencial

Class type:

Presencial