Software engineering (SE) is concerned about techniques and tools to develop software pieces. Structuring and composition techniques have always been a cornerstone in software engineering, from modules in the 70’s to the more recent component and service based approaches. These techniques support the application of the well-known divide-and-conquer approach to software development, and promote the construction of added-value software pieces by reusing existing one. More than providing a theoretical background for software engineering (which is nice, but not our objective here), formal methods (FM) support the development process and enable the automation of the whole, or parts of, the design and programming activities. In this talk, I will first present common principles of software architectures and (Web) service development. Then I will survey some of my recent works in the context of the application of formal methods to service-based software engineering. Three typical applications will be presented: software adaptation, automatic service composition, and verification (testing). Formal methods will be tackled (mainly) from a pragmatic perspective, demonstrating how, translating an issue from the SE domain to the FM domain, let state-of-the art formal verification tools do the work for the software developer.