Sistemas embarcados estão amplamente presentes em muitas aplicações inovadoras de alta tecnologia e representam um dos mercados globais de mais rápido crescimento [1]. Tais sistemas se tornaram mais robustos e complexos e, agora, exigem processadores com vários núcleos de processamento e memória compartilhada escalável, dentre outros recursos avançados, para atender à alta demanda computacional [2]. Na verdade, a cada ciclo de inovação, os sistemas embarcados devem proporcionar um melhor funcionamento com maior desempenho, ao mais baixo custo possível. Como consequência, a confiabilidade de tais sistemas torna-se um ponto-chave no processo de desenvolvimento de diversos dispositivos comerciais [3].
No caso de sistemas embarcados críticos, em que a ocorrência de falhas pode levar a consequências inaceitáveis, como grandes prejuízos materiais ou perda de vidas, assegurar a confiabilidade do software que compõe a aplicação é uma tarefa fundamental no processo. Vejamos o caso de um sistema de vídeo estereoscópico, que apresenta ao cirurgião cardiovascular a ilusão em vídeo de um coração imóvel, enquanto ele opera em um coração batendo [4]. Nesse sistema cirúrgico, é imprescindível um projeto cuidadoso de software, que assegure uma sincronização precisa e uma resposta segura. Erros em um ambiente hospitalar podem levar a lesões graves, portanto, o desenvolvimento de sistemas para esse fim deve englobar técnicas para garantir sua segurança e confiabilidade [5]. Desse modo, surge a seguinte questão:
Como podemos garantir, durante o processo de desenvolvimento, a confiabilidade dos componentes de software presentes nos sistemas embarcados críticos?
Engenheiros de software estão constantemente em busca de novas técnicas e ferramentas para auxiliar no desenvolvimento de sistemas mais robustos. Nesse contexto, os métodos de verificação formal surgem como uma abordagem promissora para alcançar tal objetivo [6]. A ideia por trás dessa técnica é construir duas representações matemáticas: uma a partir do sistema de software ou hardware (modelo) e outra a partir dos requisitos do respectivo sistema (especificações), de tal forma que se possa provar matematicamente que o modelo do sistema atende às suas especificações. Um ponto relevante é que todo processo pode ser feito de forma automática. De fato, empresas de tecnologia como a Intel [7, 8], por exemplo, investem, cada vez mais, em alternativas rápidas e baratas de verificação, a fim de averiguar a correção de seus sistemas e, portanto, evitar grandes perdas financeiras [9, 10]. No entanto, a verificação de software ainda é um assunto de intensa pesquisa na comunidade de métodos formais e sistemas embarcados [11].
Principais aspectos do processo de verificação formal de sistemas
Na tentativa de lidar com o crescimento na complexidade de tais sistemas, uma das formas mais populares, atualmente, é a abordagem conhecida como model checking [12], a qual já apresenta alguns resultados promissores na verificação de programas C++ [13, 14, 15, 16, 17, 18], linguagem amplamente utilizada no desenvolvimento de sistemas embarcados. Outra ferramenta que se destaca nesse cenário é o Java PathFinder, um verificador de modelos para detecção de bugs em programas Java e aplicações Android [19]. No entanto, apesar das inúmeras vantagens das técnicas de verificação, existem diversos tipos de sistemas que não podem ser verificados automaticamente, devido à indisponibilidade no mercado de verificadores que suportem completamente certos tipos de linguagens e frameworks. Por exemplo, a ferramenta Low-Level Bounded Model Checking (LLBMC) é capaz de verificar programas C++98, somente se todo tratamento de exceção for desconsiderado do processo de verificação [13].
Verificador de programas CUDA.
De modo particular, a linguagem C++ possui diversas funcionalidades e conceitos de orientação a objetos (OO), que tornam difícil a codificação correta dos programas em fórmulas matemáticas [20], essenciais para o processo de verificação. O principal desafio, aqui, é suportar os recursos complexos que a linguagem oferece, tais como templates, containers sequenciais e associativos, herança, polimorfismo e tratamento de exceções. Além disso, a versão C++11, em especial, dispões de diversas funcionalidades que representam grandes desafios para o processo de verificação, tais como inferência de tipo, funções lambda e recursos nativos para programação concorrente.
Curiosity Rover
Apesar das limitações, model checkers vêm apresentando resultados promissores. Por exemplo, a equipe de software de voo do Jet Laboratório de Propulsão [21] (sob contrato com NASA), utilizou extensivamente técnicas de verificação para garantir que o Rover Curiosity chegasse em Marte com sucesso em agosto de 2012 [22]. Nesse projeto, em particular, a técnica de model checking ajudou a verificar os subsistemas de software para descobrir potenciais condições de corrida de dados e deadlocks [23]. O software que controla uma nave espacial interplanetária deve ser projetado com um alto grau de confiabilidade, uma vez que, qualquer erro (por menor que seja) pode levar à perda da missão. Além disso, a Microsoft utiliza a Static Driver Verifier (SDV), uma ferramenta no Windows Driver Development Kit (integrada no Visual Studio), que usa o mecanismo de verificação do model checker SLAM (projeto para verificar se o software atende às propriedades comportamentais críticas) [24] para verificar automaticamente propriedades na API de drivers do Windows.
“A verificação de software tem sido o Santo Graal da ciência da computação por muitas décadas, mas, agora, em algumas áreas muito importantes, como por exemplo, a verificação do driver… estamos construindo ferramentas que podem fazer provas reais sobre o software e como ele funciona para garantir a sua confiabilidade.”
Bill Gates, 18 de abril de 2002. Keynote no WinHec 2002.
É importante ressaltar que a verificação formal pode ser aplicada a qualquer projeto de software ou hardware. Para saber quais tecnologias (ferramentas ou metodologias) de verificação devem ser aplicadas ao seu projeto, se pergunte: (i) O meu projeto é de hardware ou software? (ii) Como eu posso definir um modelo formal para o meu sistema e qual seria o impacto disso no processo de desenvolvimento? (iii) Como são definidos os requisitos do meu sistema? (iv) Quais linguagens de programação, ferramentas e frameworks são utilizados no processo de desenvolvimento? (v) Até que ponto o processo de verificação, dentro do meu projeto, pode ser automatizado? (vi) Tenho profissionais capacitados na minha equipe para lidar com verificação? Com base nas respostas, você terá uma boa noção de quais tecnologias deverão ser aplicadas ao seu projeto e da relação entre custo e benefício de aderir a um processo de verificação.
Apresentamos, aqui, apenas alguns pontos que evidenciam a importância da verificação formal para projetos de sistemas (hardware e software). É evidente que tais técnicas estarão cada vez mais presentes no processo de desenvolvimento de diversas aplicações. Já podemos ver seu potencial sendo aplicado em diferentes áreas de pesquisa, como verificação de redes neurais [25], verificação de sistemas ciber-físicos [26], verificação de modelos biológicos probabilísticos [27], dentre outras. Precisamos estar de olho no futuro, mas, por agora, fica o questionamento: quais alternativas vocês vêm utilizando para garantir que seus componentes de software atendam todas as especificações?
Por onde começar?
Existem várias especializações em diferentes níveis nessa área. Alguns artigos online abordam o tema de forma mais prática, como esse texto do Ulf Eriksson [28]. Indico também os livros Software Verification and Validation por Rakitin e Model Checking por Clarke, Grumberg e Peled. Para os adeptos dos cursos online, a edX tem um curso sobre Verificação Formal de Software [29].
Referências
[1] E. A. Lee and S. A. Seshia, Introduction to Embedded Systems: A Cyber-Physical
Systems Approach. http://leeseshia.org, 2015.
[2] U. Eklund, H. Holmstr¨om Olsson, and N. J. Strøm, “Industrial challenges of scaling agile in mass-produced embedded systems,” in Agile Methods. Large-Scale Development, Refactoring, Testing, and Estimation, T. Dingsøyr, N. B. Moe, R. Tonelli, S. Counsell, C. Gencel, and K. Petersen, Eds. Cham: Springer International Publishing, 2014, pp. 30–42.
[3] L. Baresi, G. Blohm, D. S. Kolovos, N. Matragkas, A. Motta, R. F. Paige, A. Radjenovic, and M. Rossi, “Formal verification and validation of embedded systems: the uml-based mades approach,” Software & Systems Modeling, vol. 14, no. 1, pp. 343–363, Feb 2015.
[4] Jocelyn Rice, “Heart Surgeons as Video Gamers,” {https://www. technologyreview.com/s/410245/heart-surgeons-as-video-gamers/}, Junho 2008, [Online; acessado em 22 de janeiro de 2018].
[5] P. Arcaini, S. Bonfanti, A. Gargantini, A. Mashkoor, and E. Riccobene, “Formal validation and verification of a medical software critical component,” in Proceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, ser. MEMOCODE ’15. Washington, DC, USA: IEEE Computer Society, 2015, pp. 80–89. [Online]. Available: https://doi.org/10.1109/MEMCOD.2015.7340473
[6] P. Cousot and R. Cousot, A Gentle Introduction to Formal Verification of Computer Systems by Abstract Interpretation. IOS Press, 2010, pp. 1–29.
[7] Slobodov´a, Anna, Challenges for Formal Verification in Industrial Setting. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 1–22.
[8] Fix, Limor, Fifteen Years of Formal Property Verification in Intel. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, ch. 8, pp. 139–144.
[9] B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and P. Schnoebelen, Systems and Software Verification: Model-Checking Techniques and Tools, 1st ed. Springer Publishing Company, Incorporated, 2010.
[10] A. Slobodová, J. Davis, S. Swords, and W. Hunt, “A flexible formal verification framework for industrial scale validation,” in Formal Methods and Models for Codesign (MEMOCODE), 2011 9th IEEE/ACM International Conference on, July 2011, pp. 89–97.
[11] R. Paludo and D. Lettnin, “A methodology for early functional verification of embedded software combining virtual platforms and bounded model checking,” in 17th Latin-American Test Symposium, LATS 2016, Foz do Iguacu, Brazil, April 6-8, 2016, 2016, pp. 141–146.
[12] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled, Model Checking. Cambridge, MA, USA: MIT Press, 1999.
[13] F. Merz, S. Falke, and C. Sinz, “Llbmc: Bounded model checking of c and c++; programs using a compiler ir,” in Proceedings of the 4th International Conference on Verified Software: Theories, Tools, Experiments, ser. VSTTE’12. Berlin, Heidelberg: Springer-Verlag, 2012, pp. 146–161. (http://llbmc.org/)
[14] J. Yang, G. Balakrishnan, N. Maeda, F. Ivanˇci´c, A. Gupta, N. Sinha, S. Sankaranarayanan, and N. Sharma, “Object Model Construction for Inheritance in C++; and Its Applications to Program Analysis,” in Proceedings of the 21st International Conference on Compiler Construction, ser. CC’12. Berlin, Heidelberg: Springer-Verlag, 2012, pp. 144–164.
[15] N. Blanc, A. Groce, and D. Kroening, “Verifying C++ with STL Containers via Predicate Abstraction,” in Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’07. New York, NY, USA: ACM, 2007, pp. 521–524.
[16] P. Prabhu, N. Maeda, and G. Balakrishnan, “Interprocedural Exception Analysis for C++,” in Proceedings of the 25th European Conference on Object-oriented Programming, ser. ECOOP’11. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 583–608. [Online]. Available: http://dl.acm.org/citation.cfm?id=2032497.2032536
[17] P. Rockai, J. Barnat, and L. Brim, “Model checking C++ with exceptions,” ECEASST, vol. 70, 2014. [Online]. Available: http://journal.ub.tu-berlin.de/ eceasst/article/view/983 (https://divine.fi.muni.cz/)
[18] F. R. Monteiro, M. A. P. Garcia, L. C. Cordeiro, and E. B. de Lima Filho, “Bounded model checking of c++ programs based on the qt cross-platform framework,” Software Testing, Verification and Reliability, pp. e1632–n/a, 2017. (http://esbmc.org/qtom)
[19] Heila van der Merwe and Brink van der Merwe and Willem Visser. Execution and Property Specifications for JPF-Android. ACM SIGSOFT Software Engineering Notes 2014; 39(1):1– 5, doi:10.1145/2557833.2560576. URL http://doi.acm.org/10.1145/2557833. 2560576. (https://babelfish.arc.nasa.gov/trac/jpf)
[20] M. Ramalho, M. Freitas, F. Sousa, H. Marques, L. Cordeiro, and B. Fischer, “SMT-Based Bounded Model Checking of C++ Programs,” in Proceedings of the 20th Annual IEEE International Conference and Workshops on the Engineering of Computer Based Systems, ser. ECBS ’13. Washington, DC, USA: IEEE Computer Society, 2013, pp. 147–156.
[21] https://www.jpl.nasa.gov/
[22] https://www.nasa.gov/mission_pages/msl/index.html
[23] G. J. Holzman, Mars Code. Commun. ACM 57(2):64-73, 2014.
[24] https://www.microsoft.com/en-us/research/project/slam/
[25] HUANG, X., KWIATKOWSKA, M., WANG, S., AND WU, M. Safety verification of deep neural networks. arXiv preprint arXiv:1610.06940 (2016).
[27] http://www.prismmodelchecker.org/
[28] https://reqtest.com/testing-blog/software-verification-and-validation-differences/
[29] https://www.edx.org/course/formal-software-verification-usmx-university-maryland-university-stv1-3x
