Business-process management (BPM) is nowadays a key technology for the automation and support of processes in medium-sized and large organizations. This technology has been successfully applied to business-to-consumer (B2C) and business-to-business (B2B) e-commerce since the ’90s, and it is now being applied also in e-government for the management of administrative procedures. As stated in Aalst, Hofstede, and Weske (2003), the origins of BPM technologies can be found in the ’70s with the research on office information systems. Research in this area was almost stopped in the ’80s, but it rose again in the ’90s under the name of work-flow management. Now it is evolving with a more integral approach and a new name: BPM. It is defined in Aalst, Hofstede, and Weske (2003, p. 4) as “supporting business processes using methods, techniques, and software to design, enact, control, and analyze operational processes involving humans, organizations, applications, documents and other sources of information.” The main functionalities provided by a BPM system are defining business processes, automatically enacting them, controlling their enactment, and analyzing them. This article is focused on the last functionality: business-process analysis (BPA). BPA can be defined as a set of technologies that provide support for obtaining relevant properties of business-process models in order to reason about them, detect functional errors, or improve their performance. BPA was a neglected area in the work-flow management systems developed in the ’90s. Will van der Aalst (1998) was one of the first researchers in this field. He proposed the use of petri nets for modeling business processes and the application of the analysis theory developed for this formalism to demonstrate the correctness of the developed processes, analyze performance, and so forth. Since then, other approaches, based on formal methods, were proposed. BPA is important for BPM because it provides the technology for improving the reliability and efficiency of the business process of organizations. Reliability considerably reduces expenses caused by errors in transactions. Efficiency reduces expenses caused by an inefficient use of resources and can improve the satisfaction of customers. The next section provides a background on the most important analysis technologies: functional verification and performance measuring. Then, the discussion is focused on functional verification. An overview on how different authors applied functional verification to business processes is presented. Then these works are analyzed and an open, modular, and extensible architecture for the functional verification of business processes is presented. Later, the future trends on this topic are outlined. Finally, the conclusion highlights the main concepts introduced in this article.