Software is virtually everywhere. As a software-based society, thinking about correctness is an important skill of the present and future software and system developers. Since Formal Methods play an important role in achieving high-trustworthiness levels, they have been directly or indirectly part of typical Computer Science education. This paper discusses and summarises impressions taken from a 10-years experience on teaching Formal Methods to undergraduate students enrolled at Computer Science and Computer Engineering courses in Brazil. At first, the topic was taught using Z and CSP# as reference languages. Over the years, for a number of reasons, the chosen languages changed to a combination of Event-B and CSPM and, at the present time, it is being taught using B. Our reflections are based on the following four perspectives: theories, tools, materials, and communities. We build on these reflections to highlight aspects that should be taken into account when designing Formal Methods modules as part of a Computer Science curriculum.

A robot affects and is affected by its environment, so that typically its behaviour depends on properties of that environment. For verification, we need to formalise those properties. Modelling the environment is very challenging, if not impossible, but we can capture assumptions. Here, we present RoboWorld, a domain-specific controlled natural language with a process algebraic semantics that can be used to define (a) operational requirements, and (b) environment interactions of a robot. RoboWorld is part of the RoboStar framework for verification of robotic systems. In this article, we define RoboWorld’s syntax and hybrid semantics, and illustrate its use for capturing operational requirements, for automatic test generation, and for proof. We also present a tool that supports the writing of RoboWorld documents. Since RoboWorld is a controlled natural language, it complements the other RoboStar notations in being accessible to roboticists, while at the same time benefitting from a formal semantics to support rigorous verification (via testing and proof).

As the world sought the 'Holy Grail' of scarless surgery, minimizing access seemed to be the natural path to follow, and minilaparoscopy (MINI) was considered to be a natural advancement of standard laparoscopy. It aims at minimizing surgical trauma by further reducing the diameter of standard instruments, without compromising range of motion, triangulation or safety. Several different terms have been coined to address this sophisticated reduced-port technique, which is characterized by the use of instruments 3 mm or less in diameter: acuscopic surgery, minilaparoscopy, needlescopic surgery and microlaparoscopy. The early adoption of MINI was mostly inhibited by the limitations of first-generation instruments, especially with respect to functionality, cost and durability. Furthermore, mini cholecystectomy demanded the use of mini optics, which suffered from poor imaging quality and a short lifetime of the scopes. Newer-generation mini instruments have mitigated these issues through the use of improved effector tips, better insulation, strength and durability, and superior optics. During the early MINI years, surgeons clipped most structures, but sturdy mini clip appliers were either unavailable or did not hold the requisite-size clips. Clipping with MINI required the use of a standard clip applier and the scope had to be changed several times during a procedure, making MINI not only more complicated but also boring and time-consuming. The development and popularization of the clipless technique allowed the surgeon to get free from the expensive and cumbersome minilaparoscopic clip appliers, and replace clips with knots. The marked improvements in instrumentation and the development of the clipless technique have occurred simultaneously with the development of NOTES, LESS and Robotic surgery, which may have contributed to a greater push towards MINI. MINI has been proven to offer more than just better cosmesis. Other advantages include better visualization of the surgical field and, with the development of precisely engineered low-friction trocars, which enhance surgical precision during dynamic and delicate tasks (knotting and suturing small structures), less stress and higher efficiency, which makes the procedure easier to perform. Furthermore, transmission of electro cautery through mini instruments has led to less lateral spread of electric current and subsequent less tissue trauma. For more than 20 years, our team has successfully used minilaparoscopy. Even with the rising popularity of robotic surgery, which still uses 8 mm instruments, minilaparoscopy remains an attractive option that is far from becoming obsolete.

Context: Test automation is often seen as a possible solution to overcome the challenges of testing mobile devices. However, most of the automation techniques adopted for mobile testing are intrusive and, sometimes, unrealistic. One possible solution for coping with intrusive and unrealistic testing is the use of robots. Despite the growing interest in the intersection between robotics and software testing, the motivations, the usefulness, and the return of investment of adopting robots for supporting testing activities are not clear. Objective: We aim at surveying the literature on the use of robotics for supporting mobile testing with a focus on the motivations, the types of tests that are automated, and the reported effectiveness/efficiency. Method: We conduct a systematic mapping study on robotic testing of mobile devices (hereafter, referred as robotic mobile testing). We searched primary studies published since 2000 by querying five digital libraries, and by performing backward and forward snowballing cycles. Results: We started with a set of 1353 papers and after applying our study protocol, we selected a final set of 20 primary studies. We provide both a quantitative analysis, and a qualitative evaluation of the motivations, types of tests automated and the effectiveness/efficiency reported by the selected studies. Conclusions: Based on the selected studies, allowing more realistic interactions is among the main motivations for adopting robotic mobile testing. The tests automated with the support of robots are usually system-level tests targeting stress, interface, and performance testing. More empirical evidence is needed for supporting the claimed benefits. Most of the surveyed work do not compare the effectiveness and efficiency of the proposed robotics-based approach against traditional automation techniques. We discuss the implications of our findings for researchers and practitioners, and outline a research agenda.

Data-flow reactive systems (DFRSs) are a class of embedded systems whose inputs and outputs are always available as signals. Input signals can be seen as data provided by sensors, whereas the output data are provided to system actuators. In previous works, verifying properties of DFRS models was accomplished in a programmatic way, with no formal guarantees, and test cases were generated by translating theses models into other notations. Here, we use Coq as a single framework to specify and verify DFRS models. Moreover, the specification of DFRSs in Coq is automatically derived from controlled natural-language requirements. Property verification is defined in both logical and functional terms. The latter allows for easier proof construction. Tests are generated with the support of the QuickChick tool. Considering examples from the literature, but also from the aerospace industry (Embraer), our testing strategy was evaluated in terms of performance and the ability to detect defects generated by mutation; within 8 seconds, we achieved an average mutation score of 75.80%.

The mini-laparoscopic cholecystectomy (MLC) was first performed in 1996, as the logical advancement of the conventional laparoscopic cholecystectomy. In Brazil, mini-laparoscopy was first performed in 1998, by Professors Peter Goh and Go Wakabaiashi, who performed a cholecystectomy using 3-mm instruments. The first study, with a considerable number of patients, was performed in Recife by Dr. Carvalho, and he reported that 719 patients were submitted to a MLC with a small rate of conversion for conventional laparoscopy. We discuss the development of mini-laparoscopy in Brazil for the past 20 years.

Background: As the minimally invasive surgery revolution approaches 30 years, many techniques are now available for cholecystectomy: open, conventional laparoscopy, ini-laparoscopy, single incision, robotic, and natural orifice. Although much has been published about patient preferences regarding these techniques, less is known about surgeon perceptions and preferences. The aim of this study was to survey attending and trainee surgeons about which cholecystectomy technique they would prefer for themselves and what factors determine their decision. Methods: Attending fellow and resident surgeons globally completed a Google Forms online questionnaire that was posted in 3 closed groups for surgeons on Facebook and WhatsApp. Results: The online questionnaire was completed by 600 surgeons (453 attending surgeons and 147 residents/fellows). Most respondents were male individuals (87.6% of attending surgeons, 78.2% of trainee surgeons). The most common age range of respondents was 31 to 40 years. Surgeon response was global, with especially good representation from North American, Asian, and European physicians. When conventional laparoscopy, mini-laparoscopy, and robotic surgery were the options offered for cholecystectomy, 58.5% of trainees and 45.7% of surgeons chose conventional laparoscopy. When asked if they would consider a single-incision or natural orifice transluminal endoscopic surgery approach, 91.5% answered no. When asked which technique they would prefer if hypothetically all techniques were equally safe, about three-fourths chose either conventional laparoscopy (46%) or mini-laparoscopy (27%). When asked to rank which factors they considered most important in choosing a surgical technique, surgeon experience (52%) and safety of the procedure (45%) were the 2 most important factors. Conclusions: When an international sample of 600 attending and trainee surgeons were asked about undergoing a cholecystectomy on themselves, most chose either conventional laparoscopy or mini-laparoscopy as their preferred access technique. Single-incision and natural orifice transluminal endoscopic surgery approaches were unpopular. Surgeons ranked the experience of the operating surgeon and safety of the procedure as the most important factors guiding their decision.

Background/objective The aim was to evaluate the use of bacterial cellulose film and bile duct autograft in repairing critical common bile duct injury in pigs. Methods A prospective experimental analytical study was carried out on 20 Sus Domesticus, Piau suidae swine, divided into a control group ( n = 10) and an experimental group ( n = 10) divided into two subgroups: bacterial cellulose film E1 and bacterial cellulose film E2 to which bacterial cellulose film was randomly allocated. The control group underwent two complete critical common bile duct sections 10 mm apart, while the experimental group with a single critical common bile duct defect underwent a 10 mm section of the longitudinal shaft with edge resection. The defects in the control group were treated with end-to-end conventional anastomosis using polyglycolic 6–0 surgical thread and the experimental group with bacterial cellulose film by continuous suture using the same material. The animals were clinically evaluated throughout the experiment on days D150 (bacterial cellulose film E1), D225 (control group), and D330 (bacterial cellulose film E2) and by intraoperative ultrasound examination related to histopathological and biochemical findings. Results The intraoperative ultrasonography detected the changes resulting from the common bile duct anastomosis in the control group that produced a considerable incidence of ductal narrowing and obstruction to the biliary flow. In the bacterial cellulose film E2 group, there was an increase in inflammation intensity, granulomatous reaction, fibrosis, and vessels density, without producing bile duct dilation in the ultrasonography assessment. Biochemical analysis of liver enzymes yielded results in the normal range confirming preservation of liver function at the different post-surgery time points. Conclusion Bacterial cellulose film, when used as a graft for bile duct repair, proved to be a biocompatible material that produced a complete healing process and biliary flow continuity.

Two female patients, one 28 years-old, and the other 61 years-old, with a history of asthenia, purpura and thrombocytopenia (both <15,000 platelets / mm3). Once other etiologies were excluded, and the diagnosis of immune thrombocytopenic purpura (ITP) was established, corticoid therapy was started in both cases. However, the patients remained with a platelet count <20,000 / mm3, characterizing refractory ITP, and the splenectomy was indicated. The surgical team opted for a hybrid minimally invasive surgical procedure. Providing a better visualization of the surgical field, less abdominal trauma, greater technical dexterity, and early hospital discharge, the use of minilaparoscopic instruments proved to be a safe and effective approach for these patients.

Objective: No data has yet been published correlating preoperative MRI staging and final TAMIS specimen pathology.The objective of this study is to report on such correlation.Methods and Procedures: All cases which were subjected to both MRI staging as well as TAMIS excision were identified.All 187 identified cases were retrospectively analyzed.The cases were performed between 2012-2019.Results: Only 39% (72/186) of cases resulted in MRI and pathological correlation.44% (83/186) of cases resulted in MRI over-staging.16% (29/186) of cases resulted in MRI under-staging.1% (2/186) of cases resulted in alternate non-suspected pathology (prostate cancer, inflammatory tissue containing staples).Conclusion: Only 39% of cases resulted in perfect correlation.44% of cases were over-staged by MRI, which could inadvertently result in eventual over-treatment.Judicious use of TAMIS excision for staging could help in reducing over-treatment.

Engagement with social media is increasing within medical professionals. There are many different platforms, such as Facebook, Instagram, Whatsapp, Twitter, Telegram, and so on. Social media is a new and important tool for surgical education. More and more surgeons are joining restricted groups to discuss surgical techniques, manuscripts, etc in a daily basis. It is important that residents and surgeons have a very critical opinion about what they look online. Not everything is good or feasible.

We describe the original technique used for the treatment of a patient who presented with pain and bulging in the abdomen, who was diagnosed with Spigelian hernia (SH) using ultrasound. In this case, the hernia occurred in the anterolateral abdominal wall with herniation of the distal ileum and mesentery, in addition to a large right inguinal hernia. A mini-laparoscopic approach was proposed; due to Child-A hepatic cirrhosis, it was done by a hybrid technique, using a harmonic scalpel. The primary closure of the hernia defects was performed, followed by the placement of a polypropylene mesh in the preperitoneal space. The mesh was fixed. In this case, the inguinal hernia was homolateral to the SH. Following the surgery, the patient had no further complications, being discharged the day after the procedure.

Defined as a group of students with common interests that gather to study a specific area of medical knowledge, the academic leagues are part of a supplementary curriculum of medical schools. In those leagues, the students have theoretical lectures, develop research projects and participate in medical activities in communities and hospitals under the supervision of medical professionals. The first Brazilian academic league (Syphilis Combat League) was created in the Medical School of the University of São Paulo in 1920.[1] The concept of the academic league has spread during the last decades, being very popular and controversial within undergraduate medicine. These leagues have the greatest responsibility for the learning of specific themes within Brazilian universities, focusing on the triad: education, research, extension.[2] Despite the huge importance of laparoscopy, medical students have a brief contact with this surgical speciality during medical school in Brazil. Usually, they get in touch with this speciality during the surgery clerkship in the last years of the medical school. Therefore, few students perform clinical research or develop interest in this area during graduation. The Academic League of Videolaparoscopy (ALVL) was created in 2010 at the University of Pernambuco, Brazil, with the objective to awaken the interest of students in laparoscopy early in the medical school, improving the development of clinical research projects, and to prepare new generations of minimally invasive surgeons. Every year, new students from the 1st to the 4th year in the medical school join the league after being selected with a multiple-question test and an analysis of the curriculum vitae. It is a 12-month programme with ten spots available per year. The activities promoted by the ALVL are: Lectures which are given weekly on minimally invasive surgery To write case reports and scientific papers and edit videos for meetings To present in regional, national and international meetings Practices: To visit the surgical centre and join the surgical team during the operations. The students are stimulated to participate in laparoscopic procedures, learning about the techniques and instruments. Moreover, there are minimally invasive surgery lectures and courses during the year. General surgery residents can also be part of the programme as tutors. They are encouraged to present lectures and to assist with research projects. Since its creation, sixty medical students had participated in the programme. Nearly 50% pursued a surgical speciality after graduation and 30% did minimally invasive surgery as a fellowship. Regarding the scientific results, the league has published 12 manuscripts in national and international journals; the students have presented more than 100 posters and videos in conferences all around the globe and received 4 international awards and 1 national award. There are several reports in the literature describing activities for medical students that provide them with opportunities for surgical skills training. Some groups, as in Russia, perform Olympiads and stimulate competition among students.[3] Patel et al. described a workshop called 'Surgery Saturday' where the students learn to suturing, knot tying and basic laparoscopic skills.[4] The students who participate in several activities provided by supplementary curriculum have an increased interest in pursuing the path to become specialised doctors. The early contact with the development of research projects and practice skills stimulates these students to look for the surgical specialities and to become researchers in the future. In our case, the students who joined the ALVL were more prone to pursue a career in surgery, and in minimally invasive surgery. Financial support and sponsorship Nil. Conflicts of interest There are no conflicts of interest.

Appendiceal tumors are rare neoplasms detected in approximately 1% of appendectomies. A 45-year-old male patient complaining of dysuria for several months, with normal urine analyses and culture, presented to the study clinic. The patient underwent a computed tomography (CT) scan that showed a cystic lesion on medium-distal cecal appendix. The surgical team opted to perform a minilaparoscopic approach. The surgery was uneventful, with a total time of 100 minutes. The patient had no further complications and was discharged 24 hours after the procedure. The minilaparoscopic approach was safe and effective in this case.

We report the cases of two patients, one 26-year-old male and one 43-year-old female, who had a history of high blood pressure and hypokalemia. The male also presented progressive tetraparesis six months before diagnosis. The female patient was diagnosed with systemic lupus erythematosus and Sjögren syndrome. After investigation, by ultrasonography and abdominal computed tomography, both patients presented hypodense and solid nodular lesions in the adrenal gland, compatible with adenoma. The surgical team opted for a hybrid minimally invasive approach. Providing a better visualization of the surgical field, less abdominal trauma, and greater technical dexterity, the use of minilaparoscopic instruments proved to be a safe and effective approach for these patients. After the surgeries, the patients presented a better control of blood pressure and electrolytes, being discharged early in good clinical conditions.

We propose a test generation strategy from natural language (NL) requirements via translation into Coloured Petri Nets (CPN), an extension of Petri Nets that supports model structuring and provides a mature theory and powerful tool support. This approach extends our previous work on the NAT2TEST framework, which involves syntactic and semantic analyses of NL requirements and the generation of Data-Flow Reactive Systems (DFRS) as an intermediate representation, from which target formal models can be obtained for the purpose of test case generation. Our contributions include automating a systematic translation of DFRSs into CPN models, an extension to deal with time aspects, besides an empirical analysis of the CPN-based test generation strategy. The analyses considered examples both from the literature (a vending machine and a nuclear power plant control system), and from the aerospace and the automotive domain (a priority command control system and a turn indicator control system, respectively). We analysed performance and the ability to detect defects generated via mutation. The results provide evidence that the contribution proposed here is more efficient, besides being able to detect at least as many defects as our previous efforts.

We propose a multi-objective strategy for finding effective inputs for fault detection in Cyber Physical Systems (CPSs). The main goal is to provide input signals for a system in such a way that they maximise the distance between the system's output and an ideal target, thus leading the system towards a fault; this is based on Genetic Algorithm and Simulated Annealing heuristics. Additionally, we take into consideration the discrete locations (of hybrid system models) and a notion of input diversity to increase coverage. We implement our strategy and present an empirical analysis to estimate its effectiveness.

A female patient, 20 years old, with a history of a progressive increase in abdominal volume on the left side, starting 3 years ago, with no associated symptoms and no history of trauma. Ultrasonography and a computed tomography scan of the abdomen were performed, which revealed a large splenomegaly, and a partial minilaparoscopic splenectomy was indicated. We opted for unroofing of the cyst, and the procedure was uneventful, with a total surgical time of 47 min. The patient progressed clinically well, without abdominal pain, being discharged on the 2(nd) post-operative day.

INTRODUCTION:This study was undertaken to identify which minimally invasive technique medical students prefer for cholecystectomy and what factors determine their decision.METHODS:Brazilian medical students watched a video reviewing the advantages and disadvantages of six different surgical approaches to cholecystectomy: open surgery, conventional laparoscopy, mini-laparoscopy (MINI), single-incision laparoscopic surgery, natural-orifice transluminal endoscopic surgery, and robotic surgery. Respondents then answered questions about hypothetical situations in which the participants would be submitted to elective cholecystectomy.RESULTS:One hundred eleven medical students completed the survey, 60 females (54%) and 51 males (46%). Most students were 19-26 years old. When asked whether they would consider an open cholecystectomy if minimally invasive surgery (MIS) techniques were available, only 9% answered yes. Senior medical students were the least willing to consider open surgery (P = .036). When asked if they would prefer conventional laparoscopy, MINI, or robotic surgery for their cholecystectomy, 85% of the women and 63% of the men chose MINI (P = .025). When asked if they would consider a single-incision laparoscopic surgery or natural-orifice transluminal endoscopic surgery approach, 94 respondents (84%) answered no. When asked to rank which factors they consider the most important when choosing a surgical technique, they ranked safety of the procedure first (58%) and surgeon experience second (30%).CONCLUSION:When Brazilian medical students were asked to select a surgical approach for cholecystectomy, most chose MINI. The preference for MINI was strongest amongst female medical students. Both female and male medical students ranked safety as the most important factor.