Uncertainty is present in software architecture decisions due to a lack of knowledge about the requirements and the solutions involved. However, this uncertainty is usually not made explicit, and decisions can be made based on unproven premises or false assumptions. This paper focuses on a technique called ArchHypo that uses hypotheses engineering to manage uncertainties related to software architecture. It proposes formulating a technical plan based on each hypothesis’ assessment, incorporating measures able to mitigate its impact and reduce uncertainty. To evaluate the proposed technique, this paper reports an application of the technique in a mission-critical project that faced several technical challenges. Conclusions were based on data extracted from the project documentation and a questionnaire answered by all team members. As a result, the application of ArchHypo provided a structured approach to dividing the architectural work through iterations, which facilitated architectural decision-making. However, further research is needed to fully understand its impact across different contexts. On the other hand, the team identified the learning curve and process adjustments required for ArchHypo's adoption as significant challenges that could hinder its widespread adoption. In conclusion, the evidence found in this study indicates that the technique has the potential to provide a suitable way to manage the uncertainties related to software architecture, facilitating the strategic postponement of decisions while addressing their potential impact.

The lack of formal foundations of UML results in imprecise models since UML only defines graphical notations, but not their formal semantics. However, in safety-critical applications, formal semantics is a requirement for verification. Semantics for the key parts of activities and classes of UML is defined by the semantics of a foundational subset for executable UML models (fUML). Moreover, the base semantics given by fUML defines the formal semantics of UML. In this paper, we evaluate a subset of the base semantics given by fUML covering its formal definition and its use for verification. From the practical perspective, we show with a simple example how the base semantics can support formal verification through theorem proving. The initial results show that the base semantics, when mature, can play an important role in the formal verification of UML models.